proposition: Lemma gorg_refl n : reflect (gorgeous n) (gorgeous_b n).
proof: Proof. case: n=>/=[|n]; first by constructor; apply:g_0. case: n=>/=[|n]; first by constructor; apply: not_g1. case: n=>/=[|n]; first by constructor; apply: not_g2. case: n=>/=[|n]. - constructor; apply:(g_plus3 _ 0); first by apply g_0. by rewrite add0n. case: n=>/=[|n]; first by constructor; apply: not_g4. case: n=>/=[|n]. - constructor; apply:(g_plus5 _ 0); first by apply g_0. by rewrite add0n. case: n=>/=[|n]. - constructor; apply:(g_plus3 _ 3)=>//. apply:(g_plus3 _ 0); first by apply g_0. by rewrite add0n. case: n=>/=[|n]; first by constructor; apply: not_g7. suff X: (n.+4.+4 >= 8); last by []. by apply:(gorg_refl'). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)