proposition: Theorem bdiv_aux_correct2 : forall b m n:nat, m <= b -> 0 < n -> snd (bdiv_aux b m n) < n.
proof: Proof. intros b; induction b as [ | b Hrec]; auto with arith. { cbn in |- *; intros m n Hle Hlt; case (le_gt_dec n m). - generalize (Hrec (m - n) n). case (bdiv_aux b (m - n) n); simpl in |- *; intros; lia. - simpl in |- *; intros; lia. } Qed.
imports: Arith Lia