proposition: Lemma beautiful_gorgeous (n: nat) : beautiful n -> gorgeous n.
proof: Proof. elim=>n'{n}=>//. - by move=>->; apply g_0. - by move=>->; apply: (g_plus3 _ 0)=>//; apply g_0. - by move=>->; apply: (g_plus5 _ 0)=>//; apply g_0. move=> n m H1 H2 H3 H4->{n'}. elim: H2; first by move=>_->; rewrite add0n. by move=> n' m' H5 H6->; rewrite addnAC; apply: (g_plus3 _ (m' + m)). by move=> n' m' H5 H6->; rewrite addnAC; apply: (g_plus5 _ (m' + m)). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)