proposition: Lemma bdiv_aux_correct2 : forall b m n:nat, m <= b -> 0 < n -> snd (bdiv_aux b m n) < n.
proof: Proof. intros b; elim b; simpl;auto. intros b' Hrec m n Hleb Hlt; case (le_gt_dec n m); simpl; auto. intros Hle; generalize (Hrec (m-n) n); case (bdiv_aux b' (m-n) n); simpl; intros q r Hrec'. apply Hrec'; [lia | auto]. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure