proposition: Lemma gorgeous_beautiful (n: nat) : gorgeous n -> beautiful n.
proof: Proof. elim=>{n} -n=>//. - by move=>->; apply: b_0. - move=>m H1 H2->{n}. by move: (b_sum (m + 3) m 3 H2)=>H; apply: H=>//; apply: b_3. - move=>m H1 H2->{n}. by move: (b_sum (m + 5) m 5 H2)=>H; apply: H=>//; apply: b_5. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)