proposition: Lemma Xmul_Xinv : forall x, Xmul x (Xinv x) = Xmask (Xreal 1) (Xinv x).
proof: Proof. intros [|x] ; try easy ; simpl ; unfold Xinv'. destruct (is_zero_spec x). apply refl_equal. apply (f_equal Xreal). now apply Rinv_r. Qed.
imports: Coq(Reals Bool) Flocq(Raux) mathcomp.ssreflect(ssreflect) Stdlib