proposition: Lemma div_eucl_eq a b : b<>0 -> let (q, r) := div_eucl a b in a = b * q + r.
proof: Proof. destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial; (now destruct 1) || intros _; generalize (pos_div_eucl_eq a (pos b) Logic.eq_refl); destruct pos_div_eucl as (q,r); rewrite mul_comm. - trivial. - intros ->. destruct r as [ |r|r]; rewrite <- !mul_opp_comm; trivial; rewrite mul_add_distr_l, mul_1_r, <- add_assoc; f_equal; now rewrite add_assoc, add_opp_diag_r. - change (neg a) with (- pos a). intros ->. rewrite (opp_add_distr _ r), <- mul_opp_r. destruct r as [ |r|r]; trivial; rewrite opp_add_distr, mul_add_distr_l, <- add_assoc; f_equal; unfold sub; now rewrite add_assoc, mul_opp_r, mul_1_r, add_opp_diag_l. - change (neg a) with (- pos a). intros ->. now rewrite opp_add_distr, <- mul_opp_l. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass