proposition: Theorem bdiv_aux_correct1 : forall b m n:nat, m <= b -> 0 < n -> m = fst (bdiv_aux b m n) * n + snd (bdiv_aux b m n).
proof: Proof. intros b; elim b; simpl. - intros m n Hle; inversion Hle; 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'. rewrite <- Nat.add_assoc; rewrite <- Hrec'; auto with arith. lia. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure