proposition: Lemma nds_FA_21: nds_FA \2c \1c = \2c.
proof: Proof. move: (nds_FA_def NS2 clt_01 cle_12);rewrite nds_f2. set v := (nds_FA \2c \1c);move => [vN lv2 ha hb]. apply: (cleA lv2). move:(nds_card_different_deg NS1). rewrite succ_one (cpowx1 CS2); move => [r1 r2]. suff foo: nds_type oopow \2c \1c by rewrite - r2; exact: (ha _ r1 foo). split; first by move => i li2; exact (oopow_pos (OS_cardinal (proj31_1 li2))). have e0:= OS0. exists \0c; split => //. move => i /proj31_1/ OS_cardinal oi. by rewrite (odegree_opow oi); apply: ole0x. apply/set_of_card_oneP; exists \0c; apply: set1_pr. by apply: (Zo_i inc_C0_C2); rewrite (odegree_opow e0). by move => t /Zo_P [/C2_P]; case => -> //; rewrite (odegree_opow OS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)