proposition: Lemma quot_rem' a b : a = b*(a÷b) + rem a b.
proof: Proof. rewrite mul_comm. generalize (quotrem_eq a b). unfold quot, rem. now destruct quotrem. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass