proposition: Lemma repr3 n : n >= 8 -> exists k, [\/ n = 3 * k + 8, n = 3 * k + 9 | n = 3 * k + 10].
proof: Proof. elim: n=>// n Ih. rewrite leq_eqVlt; case/orP. - by rewrite eqSS=>/eqP<-; exists 0; rewrite muln0 add0n; constructor. case/Ih=>k; case=>->{n Ih}. - by exists k; constructor 2; rewrite -addn1 -addnA addn1. - by exists k; constructor 3; rewrite -addn1 -addnA addn1. exists (k.+1); constructor 1. by rewrite mulnSr -addn1 -2!addnA; congr (_ + _). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)