proposition: Lemma mul1 x : 1 * x == x.
proof: Proof. elim/opp_ind: x => [x IHx | x le0x]. by apply eqR_opp2; rewrite -IHx mulRN. rewrite ge0_mul //; split=> [b /open[a ltxa ltab] | b [a [lt1a _] ltxba]]. have a_gt0: 0 < a by apply/leRq: (a) ltxa. by rewrite amulC; exists a; rewrite ge0_abs // ltcE ltr_pdivl_mulr ?mul1r. have a_gt0: 0 < a by apply: lt_trans lt1a. have b_gt0: 0 < b by rewrite ltcE -(mul0r a) -ltr_pdivl_mulr ?(abs_ge0 ltxba). rewrite -[x]ge0_abs //; apply: ltc_trans ltxba _. by rewrite gtr_pmulr ?invf_lt1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)