proposition: Lemma leqn1 n: (n <=1) = (n==0) || (n ==1).
proof: Proof. by rewrite leq_eqVlt orbC ltnS leqn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)