proposition: Lemma mulC x y : x * y == y * x.
proof: Proof. by rewrite /mul [_ <-> _]and_comm amulC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)