proposition: Theorem div_eucl_spec a b : let (q,r) := div_eucl a b in a = b * q + r.
proof: Proof. destruct a as [|a], b as [|b]; unfold div_eucl; trivial. generalize (pos_div_eucl_spec a (pos b)). destruct pos_div_eucl. now rewrite mul_comm. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties