proposition: Lemma Xdiv_0_r : forall x, Xdiv x (Xreal 0) = Xnan.
proof: Proof. intros [|x] ; try easy ; simpl ; unfold Xdiv'. case is_zero_spec. easy. intros H. now elim H. Qed.
imports: Coq(Reals Bool) Flocq(Raux) mathcomp.ssreflect(ssreflect) Stdlib