proposition: Lemma amulC x y : `|x|*|y| == `|y|*|x|.
proof: Proof. without loss suffices: x y / `|y|*|x| <= `|x|*|y| by []. move=> b [a ltxa ltyba]; exists (b / a)%R; rewrite // invf_div mulrC divfK //. by rewrite gt_eqF // -(mul0r a) -ltr_pdivl_mulr (abs_ge0 ltxa, abs_ge0 ltyba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)