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