proposition: Lemma not_g7: ~(gorgeous 7).
proof: Proof. case=>//n Ih /eqP; case: n Ih=>//n Ih; rewrite addnC !eqSS; move/eqP=>Z; subst n. - by apply:not_g4. by apply:not_g2. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)