proposition: Lemma CNFB_bound_p X: CNFB_ax X -> inc X (CNFB_bound (CNFBv X)).
proof: Proof. move => [p1 p2 p3 p4]. apply:(fgraph_bd p1 p2) => i idx. move: (props_of_b) => [ob bnz bp]. move: (p4) => [[p11 p12 p13 p14] p15]. move/(NltP p2): (idx) => lt1. have la: inc (ocoef X i) gamma by move:(p13 i lt1) => /(oltP ob). rewrite - (p3 _ idx) -/(oexp _ _) -/(ocoef _ _); apply: (setXp_i) la. move: (OS_CNFq p2 (proj1 p4)) => osx. apply/(oleP osx). have ot:= (p12 _ lt1). apply: (oleT (oleT (oprod_M1le bp ot)(opow_Mspec2 ot bg2))). case: (equal_or_not (domain X) \0c) => nz. by move: lt1; rewrite nz => /clt0. move: (cpred_pr p2 nz) => [mN mv]. rewrite mv in p4 lt1. move:(CNFq_pg4 mN p4); rewrite - mv => eq1. have aa: i <=c (cpred (domain X)) by apply /(cltSleP mN). have bb:=(cltS mN). move: (CNF_exponents_M (NS_succ mN) (proj1 p4) aa bb) => /(opow_Meqle bp). by move => hc; apply: (oleT hc eq1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)