proposition: Lemma log32 : log 32 = 5.
proof: Proof. rewrite (_ : 32 = 2 ^ 5); last lra. rewrite /log Log_expR // /Log divRR ?ln2_neq0 // mulR1 !S_INR add0R; field. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext