proposition: Theorem pos_div_eucl_spec (a:positive)(b:N) : let (q,r) := pos_div_eucl a b in pos a = q * b + r.
proof: Proof. induction a as [a IHa|a IHa|]; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. - destruct pos_div_eucl as (q,r). change (pos a~1) with (succ_double (pos a)). rewrite IHa, succ_double_add, double_mul. case leb_spec; intros H; trivial. rewrite succ_double_mul, <- add_assoc. f_equal. now rewrite (add_comm b), sub_add. - destruct pos_div_eucl as (q,r). change (pos a~0) with (double (pos a)). rewrite IHa, double_add, double_mul. case leb_spec; intros H; trivial. rewrite succ_double_mul, <- add_assoc. f_equal. now rewrite (add_comm b), sub_add. - now destruct b as [|[ | | ]]. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties