proposition: Lemma pos_div_eucl_bound a b : 0<b -> 0 <= snd (pos_div_eucl a b) < b.
proof: Proof. assert (AUX : forall m p, m < pos (p~0) -> m - pos p < pos p). { intros m p. unfold lt. rewrite (compare_sub m), (compare_sub _ (pos _)). unfold sub. rewrite <- add_assoc. simpl opp; simpl (neg _ + _). now rewrite Pos.add_diag. } intros Hb. destruct b as [|b|b]; discriminate Hb || clear Hb. induction a as [a IHa|a IHa|]; unfold pos_div_eucl; fold pos_div_eucl. - destruct pos_div_eucl as (q,r). simpl in IHa; destruct IHa as (Hr,Hr'). case ltb_spec; intros H; unfold snd; split. + now destruct r. + trivial. + unfold le. now rewrite compare_antisym, <- compare_sub, <- compare_antisym. + apply AUX. rewrite <- succ_double_spec. destruct r; try easy. unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, Hr'. - destruct pos_div_eucl as (q,r). simpl in IHa; destruct IHa as (Hr,Hr'). case ltb_spec; intros H; unfold snd. + split; trivial. now destruct r. + split. * unfold le. now rewrite compare_antisym, <- compare_sub, <- compare_antisym. * apply AUX. destruct r; try easy. - case leb_spec; intros H; simpl; split; try easy. red; simpl. now apply Pos.le_succ_l. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass