proposition: Lemma trunc_lognn p : 1 < p -> trunc_log p p = 1.
proof: Proof. by case: p => [|[|p]] // _; rewrite /trunc_log ltnSn divnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)