proposition: Lemma mulA x y z : x * (y * z) == x * y * z.
proof: Proof. elim/opp_ind: x => [* | x le0x]; first by apply: eqR_opp2; rewrite -!mulNR. elim/opp_ind: y => [y IHy | y le0y]. by apply: eqR_opp2; rewrite -mulRN -mulNR IHy mulRN mulNR. elim/opp_ind: z => [* | z le0z]; first by apply: eqR_opp2; rewrite -!mulRN. by rewrite !ge0_mul ?amulA //; apply: amul_ge0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)