proposition: Lemma axioms : Real.axioms structure.
proof: Proof. move: leRR leR_trans sup_ub sup_total add_monotony addC addA add0 addN. by move: mul_monotony mulC mulA mulDr mul1 mulV; split=> //= -[/leRq[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)