proposition: Lemma natural_small x y e (v := oopow e): ordinalp e -> x <o v -> y <o v -> (x +#o y) <o v.
proof: Proof. move => oe qa qb. have ox:= proj31_1 qa. have oy:= proj31_1 qb. case: (ozero_dichot ox); first by move ->; rewrite natural_sumC natural_sum0. case: (ozero_dichot oy); first by move ->; rewrite natural_sum0. move => yp xp. move: (the_cnf_p6 oe xp qa) (the_cnf_p6 oe yp qb). rewrite /odegree (Y_false (nesym (proj2 xp))) (Y_false (nesym (proj2 yp))). move => dx dy. move: (olt_leT xp (ord_compare_nat_sum1 ox oy)) => zp. suff: odegree (x +#o y) <o e. move/oleSltP => /opow_Mo_le; apply: olt_leT. exact: (proj2 (the_cnf_p4 zp)). move: (proj1 (the_cnf_p0_nz zp)). rewrite /odegree (Y_false (nesym (proj2 zp))) /natural_sum. move: (the_cnf_p0 ox)(the_cnf_p0 oy) =>[oa av][ob bv]. rewrite (proj43 (cnf_and_val_pb (cnfp_nat_sum oa ob))). set s := (the_cnf x +#f the_cnf y) => sp. have : inc (cnf_degree s) (cnf_exponents s). apply/funI_P; exists (Vg s (cnf_size s)) => //. by apply: (inc_V_range (proj41 (proj1 sp)) (cnf_size_nz_bis sp) ). rewrite (cnf_nat_sum_p1 oa ob); case/setU2_P => /funI_P [t tr ->]. move/(range_gP (proj41 oa)): tr => [i idx ->]. exact: (ole_ltT (cnf_degree_greatest oa idx) dx). move/(range_gP (proj41 ob)): tr => [i idx ->]. exact: (ole_ltT (cnf_degree_greatest ob idx) dy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)