<exp_S <plus_minus_m_m [2:@lt_O_log //]
-Hind #Hind <Hclog @(transitive_le … Hind)
>(eq_log_exp … (le_n ?)) >(eq_log_exp … (le_n ?))
<exp_S <plus_minus_m_m [2:@lt_O_log //]
-Hind #Hind <Hclog @(transitive_le … Hind)
>(eq_log_exp … (le_n ?)) >(eq_log_exp … (le_n ?))