proposition: Lemma amul0 x : `|0|*|x| == 0.
proof: Proof. split=> [a a_gt0|]; last exact/leRq/amul_ge0. have [b lexb] := cut_ub `|x|; have b_gt0 := abs_ge0 lexb. exists (a / b)%R; first by rewrite ltcE /abs_cut opp0 ltcE divr_gt0. by rewrite invfM invrK mulVKf ?gt_eqF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)