+theorem divides_to_divides_b_true1 : \forall n,m:nat.
+O < m \to n \divides m \to divides_b n m = true.
+intro.
+elim (le_to_or_lt_eq O n (le_O_n n))
+ [apply divides_to_divides_b_true
+ [assumption|assumption]
+ |apply False_ind.
+ rewrite < H in H2.
+ elim H2.
+ simplify in H3.
+ apply (not_le_Sn_O O).
+ rewrite > H3 in H1.
+ assumption
+ ]
+qed.
+