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