proposition: Lemma Xinv_Xmul_distr : forall x y, Xinv (Xmul x y) = Xmul (Xinv x) (Xinv y).
proof: Proof. intros [|x] [|y] ; try easy ; simpl ; unfold Xinv'. now destruct (is_zero_spec x). destruct (is_zero_spec x). destruct (is_zero_spec (x * y)). apply refl_equal. elim H0. rewrite H. apply Rmult_0_l. destruct (is_zero_spec y). destruct (is_zero_spec (x * y)). apply refl_equal. elim H1. rewrite H0. apply Rmult_0_r. destruct (is_zero_spec (x * y)). elim (prod_neq_R0 _ _ H H0 H1). apply (f_equal Xreal). now apply Rinv_mult_distr. Qed.
imports: Coq(Reals Bool) Flocq(Raux) mathcomp.ssreflect(ssreflect) Stdlib