proposition: Lemma Z_div_mod_eq : forall a b : Z, (b > 0)%Z -> a = (b * (a / b) + a mod b)%Z.
proof: Proof. intros a b H. apply Z_div_mod_eq_full ; now apply Zaux.Zgt_not_eq, Z.gt_lt. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux) Coquelicot.Coquelicot