proposition: Theorem div_mod' a b : a = b * (a/b) + (a mod b).
proof: Proof. generalize (div_eucl_spec a b). unfold div, modulo. now destruct div_eucl. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties