proposition: Theorem pos_div_eucl_remainder (a:positive) (b:N) : b<>0 -> snd (pos_div_eucl a b) < b.
proof: Proof. intros Hb. 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); simpl in *. case leb_spec; intros H; simpl; trivial. apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial. destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ]. apply (succ_double_lt _ _ IHa). - destruct pos_div_eucl as (q,r); simpl in *. case leb_spec; intros H; simpl; trivial. apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial. destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ]. now destruct r. - destruct b as [|[ | | ]]; easy || (now destruct Hb). Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties