proposition: Lemma gorg_criteria n : n >= 8 -> gorgeous n.
proof: Proof. case/repr3=>k; case=>->{n}. - apply: (g_plus5 _ (3*k + 3)); last by rewrite -addnA. by apply: (g_plus3 _ (3*k))=>//; apply: gorg3. - apply: (g_plus3 _ (3*k + 6))=>//; last by rewrite -addnA. apply: (g_plus3 _ (3*k + 3))=>//; last by rewrite -addnA. by apply: (g_plus3 _ (3*k))=>//; apply: gorg3. apply: (g_plus5 _ (3*k + 5))=>//; last by rewrite -addnA. by apply: (g_plus5 _ (3*k))=>//; apply: gorg3. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)