WIP / Experiment : Remove the dependency on R#112

Closed

drouhling wants to merge 11 commits into

Commits on Oct 3, 2018

Remove ball and absRingType
damien rouhling
committed
Shorten proofs
damien rouhling
committed
Use {ereal R} in hierarchy
damien rouhling
committed

Commits on Oct 4, 2018

Reintroduce lemmas about R that were commented out
damien rouhling
committed

Commits on Oct 8, 2018

Add and use a theory of max using bigop
damien rouhling
committed

Commits on Oct 9, 2018

Add min using bigop and simplify proofs
damien rouhling
committed
Move and extend Rstruct.v
damien rouhling
committed

Commits on Oct 10, 2018

Clean up
damien rouhling
committed

Commits on Oct 12, 2018

More clean up
damien rouhling
committed
Rework documentation and mark missing lemmas
damien rouhling
committed
Reintroduce missing lemmas + more clean up
damien rouhling
committed