proposition: Fact amul_is_cut x y : is_cut (amul_cut x y).
proof: Proof. split=> [|| a b [c ltxc ltyac] ltab | a [b ltxb /open[c ltyc ltcab]]]. - have [[a ltxa] [b ltyb]] := (cut_ub `|x|, cut_ub `|y|). by exists (b * a)%R, a; rewrite ?mulfK ?gt_eqF // (abs_ge0 ltxa). - by exists 0%R => -[a _ /abs_ge0]; rewrite mul0r ltcE ltxx. - exists c => //; have c_gt0: 0 < c := abs_ge0 ltxc. by apply: ltc_trans ltyac _; rewrite ltr_pmul2r ?invr_gt0. have b_gt0: 0 < b := abs_ge0 ltxb. by exists (c * b)%R; first exists b; rewrite -?ltr_pdivl_mulr ?mulfK ?gt_eqF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)