] #Hcut
@le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus <Hplus >S_pred
[>eq_minus_S_pred in ⊢ (??%); >S_pred
] #Hcut
@le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus <Hplus >S_pred
[>eq_minus_S_pred in ⊢ (??%); >S_pred
>commutative_times in ⊢ (? (? (? % ?) ?) ?);
>associative_times @monotonic_le_times_r
<exp_plus_times @(le_exp … (lt_O_S ?))
>commutative_times in ⊢ (? (? (? % ?) ?) ?);
>associative_times @monotonic_le_times_r
<exp_plus_times @(le_exp … (lt_O_S ?))
[normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n
|@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
]
[normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n
|@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
]
[@lt_O_S |@(le_times_to_le 2) [@lt_O_S |<Hm @lt_to_le @lem]]
|<Hm <exp_plus_times @(le_exp … (lt_O_S ?))
whd in match (times 2 m); >commutative_times <times_n_1
[@lt_O_S |@(le_times_to_le 2) [@lt_O_S |<Hm @lt_to_le @lem]]
|<Hm <exp_plus_times @(le_exp … (lt_O_S ?))
whd in match (times 2 m); >commutative_times <times_n_1