proposition: Lemma Xdiv_split : forall x y, Xdiv x y = Xmul x (Xinv y).
proof: Proof. intros [|x] [|y] ; try split. unfold Xbind2, Xbind, Xdiv', Xinv'. now case (is_zero y). Qed.
imports: Coq(Reals Bool) Flocq(Raux) mathcomp.ssreflect(ssreflect) Stdlib