#b #lt1b @nat_elim2 normalize
[#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
|#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))
#b #lt1b @nat_elim2 normalize
[#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
|#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))