proposition: Lemma exp3n n : (3 ^ n)%N = (3 ^ n).-1.+1.
proof: Proof. by elim: n => // n IHn; rewrite expnS IHn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)