proposition: Lemma Xmul_assoc : forall x y z, Xmul (Xmul x y) z = Xmul x (Xmul y z).
proof: Proof. intros [|x] [|y] [|z] ; try split. simpl. apply f_equal. apply Rmult_assoc. Qed.
imports: Coq(Reals Bool) Flocq(Raux) mathcomp.ssreflect(ssreflect) Stdlib