proposition: Lemma one_not_beautiful n: n = 1 -> ~ beautiful n.
proof: Proof. move=>E H. elim: H E=>n'; do?[by move=>->]. move=> n1 m' _ H2 _ H4 -> {n' n}. case: n1 H2=>// n'=> H3. by case: n' H3=>//; case. Qed.
imports: mathcomp(ssreflect eqtype ssrnat ssrbool ssrfun seq)