proposition: Lemma nds_card_different_deg n: natp n -> nds_ax oopow (csucc n) /\ nds_card oopow (csucc n) = \2c ^c n.
proof: Proof. move => nN. have ha: opos_below oopow (csucc n). by move => y tn; apply: oopow_pos; exact: (proj1 (proj31_1 tn)). have hb i j: i <c j -> j <=c n -> odegree (oopow i) <o odegree (oopow j). move => /oclt lij _. by rewrite (odegree_opow (proj31_1 lij)) (odegree_opow (proj32_1 lij)). exact: (nds_card_different_deg_gen nN ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)