proposition: Lemma g_times2 (n: nat): gorgeous n -> gorgeous (n * 2).
proof: Proof. rewrite muln2. elim=>{n}[n Z|n m H1 H2 Z|n m H1 H2 Z]; subst n; first by rewrite double0; apply g_0. - rewrite doubleD -(addnn 3) addnA. by apply: (g_plus3 _ (m.*2 + 3))=>//; apply: (g_plus3 _ m.*2)=>//. rewrite doubleD -(addnn 5) addnA. by apply: (g_plus5 _ (m.*2 + 5))=>//; apply: (g_plus5 _ m.*2)=>//. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)