proposition: Lemma div_mod a b : b<>0 -> a = b*(a/b) + (a mod b).
proof: Proof. intros Hb. generalize (div_eucl_eq a b Hb). unfold div, modulo. now destruct div_eucl. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass