+theorem divides_b_true_to_divides:
+\forall n,m:nat. divides_b n m = true \to n \divides m.
+intros 2.apply (nat_case n)
+ [apply (nat_case m)
+ [intro.apply divides_n_n
+ |simplify.intros.apply False_ind.
+ apply not_eq_true_false.apply sym_eq.assumption
+ ]
+ |intros.
+ apply divides_b_true_to_divides1
+ [apply lt_O_S|assumption]
+ ]
+qed.
+
+theorem divides_b_false_to_not_divides1: