proposition: Lemma pos_div_eucl_eq a b : 0 < b -> let (q, r) := pos_div_eucl a b in pos a = q * b + r.
proof: Proof. intros Hb. induction a as [a IHa|a IHa|]; unfold pos_div_eucl; fold pos_div_eucl. - destruct pos_div_eucl as (q,r). change (pos a~1) with (2*(pos a)+1). rewrite IHa, mul_add_distr_l, mul_assoc. destruct ltb. + now rewrite add_assoc. + rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal. unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r. - destruct pos_div_eucl as (q,r). change (pos a~0) with (2*pos a). rewrite IHa, mul_add_distr_l, mul_assoc. destruct ltb. + trivial. + rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal. unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r. - case leb_spec; trivial. intros Hb'. destruct b as [|b|b]; try easy; clear Hb. replace b with 1%positive; trivial. apply Pos.le_antisym. + apply Pos.le_1_l. + now apply Pos.lt_succ_r. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass