proposition: Lemma oprod2_comm5 a b (x := cnf_val a) (y := cnf_val b): cnfp_nz a -> cnfp_nz b -> oexp a \0c = \0o -> oexp b \0c = \0o -> cnf_size a = \0c -> oprod_comm x y -> (x = \1o \/ (x <o omega0 /\ y <o omega0)).
proof: Proof. move=> anz bnz limX limY sz cxy. move:(cnf_nat_prop anz sz limX)=> [fx xv]. have bN:= (proj42 (proj1 bnz)). case: (equal_or_not (cnf_size b) \0c) => sbz. right; split; [ exact | exact: (proj1 (cnf_nat_prop bnz sbz limY))]. move: (cnfp_prod_gen anz bnz). move: (cnfp_prod_gen bnz anz). move:(CNF_prod_pr6 anz bnz limY). move:(CNF_prod_pr6 bnz anz limX). set u := cnf_prod_gen a b. set v := cnf_prod_gen b a. move => eq1 eq2 ov ou. have eq3: cnf_val u = cnf_val v by rewrite - eq1 - eq2. move:(cnf_val_inj ou ov eq3) => eq4. left; rewrite /x xv; clear eq1 eq2 eq3 cxy. move:(cnf_size_nz bnz) => [qa qb]. have pdy: (domain b -c \1c) = cnf_size b. by rewrite - (cpred_pr4 (CS_nat bN)) qb (cpred_pr1 (CS_nat qa)). have db0: domain b +c \0c = domain b. rewrite csum0r // qb; fprops. move: (proj2(cnf_size_nz anz)); rewrite sz succ_zero => da. have da1: domain a -c \1c = \0c by rewrite da cdiff_nn. have [zdb lzdb] := cnf_size_nz_ter bnz. have [zda lzda] := cnf_size_nz_ter anz. have eq1: (domain a +c (domain b -c \1c)) = domain b. by rewrite pdy da csumC qb - (csucc_pr4 (CS_nat qa)). move:(f_equal (Vg ^~ \0c) eq4). rewrite/u/v/cnf_prod_gen/cnf_nm !Lgd. rewrite/cnf_ns /cnf_nck/cnf_m eq1 da1 db0 (LgV zdb) (LgV zdb) (LgV zda). rewrite (LgV zdb);Ytac0; Ytac0. rewrite /cnf_c sz;Ytac0; Ytac0 => /(f_equal Q); aw. move/cnfpP: (proj1 bnz) => /proj43 h. move: (proj33 (h _ zdb))=>[cN /proj2/nesym cp]. rewrite -(cprod1l (CS_nat cN)). move/ (cprod_eq2r cN (proj1 (posnat_lc anz)) NS1 cp). by rewrite/cnf_lc sz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)