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