proposition: Lemma ge0_mul x y : x >= 0 -> y >= 0 -> x * y == `|x|*|y|.
proof: Proof. by rewrite /mul => le0x le0y; case: ifR_cases => [|[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)