Induction: evenb_n__oddb_Sn
Induction: ble_nat_refl
Induction: zero_nbeq_S
Induction: andb_false_r
Induction: plus_ble_compat_l
Induction: S_nbeq_0
Induction: mult_1_l
Induction: all3_spec
Induction: mult_plus_distr_r
Induction: mult_assoc