proposition: Lemma mulDr x y z : x * (y + z) == x * y + x * z.
proof: Proof. elim/opp_ind: x => [x IHx | x le0x]. by apply/eqR_opp2; rewrite oppD -!mulNR IHx. elim/opp_ind: y => [y IHy | y le0y] in z *. by apply/eqR_opp2; rewrite oppD -!mulRN oppD IHy. without loss le0z: y z le0y / z >= 0. move=> IHz; have [/gec0_opp-le0nz | /(IHz y)->//] := ltcP z 0. move Dt: (y + z) => t; have {} Dt: y + z == t by rewrite Dt. elim/opp_ind: t => [t IHt | t le0t] in y z Dt le0y le0nz *. by apply/eqR_opp2; rewrite oppD -!mulRN addC -IHt ?oppK // addC -oppD Dt. rewrite -(add0 (x * t)) -(addN (x * z)) -mulRN -addA -{}IHz //. by rewrite addC -Dt (addC y) addA -(addC z) addN add0. have [/leRq-leR0y /leRq-leR0z] := (le0y, le0z). have le0yz: y + z >= 0 by move/(add_monotony leR0z); rewrite addC add0. rewrite !ge0_mul //; symmetry; split=> [c [a ltxa] | c [d [a1 ltxa1]]]. rewrite ge0_abs // => -[b ltyb ltz_cab]; have a_gt0 := abs_ge0 ltxa. exists (b * a)%R, a => //; first by rewrite mulfK ?gt_eqF // ge0_abs. by rewrite mulrBl mulfK ?gt_eqF // ge0_abs. rewrite ge0_abs // => lty_da1 [a2]; rewrite (ge0_abs le0z) // => ltxa2 ltz_cda2. have [a ltxa [lea1 lea2]]: exists2 a, `|x| < a & (a <= a1)%R /\ (a <= a2)%R. exists (Num.min a1 a2); first by rewrite fun_if; case: ifP. by apply/andP; rewrite -lexI. have [[a_gt0 a1_gt0] a2_gt0] := (abs_ge0 ltxa, abs_ge0 ltxa1, abs_ge0 ltxa2). have dgt0: 0 < d by move/leR0y: lty_da1; rewrite ltcE pmulr_lgt0 ?invr_gt0. have cdgt0: 0 < c - d. by move/leR0z: ltz_cda2; rewrite ltcE pmulr_lgt0 ?invr_gt0. exists a; rewrite // (ge0_abs le0yz); exists (d / a)%R; last rewrite -mulrBl. by apply: ltc_le_trans lty_da1 _; rewrite ler_pmul2l ?lef_pinv. by apply: ltc_le_trans ltz_cda2 _; rewrite ler_pmul2l ?lef_pinv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)