proposition: Lemma oprod2_comm1 a b (x := cnf_val a) (y:= cnf_val b): cnfp_nz a -> cnfp_nz b -> oexp b \0c = \0o -> \0o <o oexp a \0c -> oprod_comm x y -> y = \1o.
proof: Proof. move => anz bnz ha hb eq1. move: (cnfp_prod_gen anz bnz). move: (cnfp_shift_expo (proj1 anz) (OS_cnf_degree bnz)). set u := cnf_shift_expo a (cnf_degree b). set v := cnf_prod_gen a b. move => ou ov. have eq2: cnf_val v = cnf_val u. by rewrite -(CNF_prod_pr5 bnz anz hb) - (CNF_prod_pr6 anz bnz ha). move:(cnf_val_inj ov ou eq2) => eq3. move: (proj42 (proj1 anz)) (proj42 (proj1 bnz)) => aN bN. 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)). move: (f_equal domain eq3). rewrite/u/v/cnf_prod_gen/cnf_shift_expo /cnf_nm Lgd. rewrite /cnf_nck /cnf_ns ! Lgd => eq4. move: (eq4); rewrite pdy - {2}(csum0r (CS_nat aN)). move/(csum_eq2l aN qa NS0) => eq5. rewrite /y (proj2 (cnf_nat_prop bnz eq5 ha)). move:(cnf_size_nz_bis anz) => qe. have qf: cnf_size a <c domain a by apply/NltP. move:(f_equal (Vg^~ (cnf_size a)) eq3). rewrite/u/v /cnf_prod_gen /cnf_nm /cnf_shift_expo !Lgd eq4. rewrite (LgV qe) (LgV qe) /cnf_m /cnf_nck /cnf_c; Ytac0. rewrite (LgV qe); Ytac0 => /pr2_def. move:(posnat_lc anz) => [q1 /proj2/nesym q2]. move:(proj1 (posnat_lc bnz)); rewrite/(cnf_lc) eq5=> aux. rewrite -/(cnf_lc a) - {2} (cprod1r (CS_nat q1)). by move/(cprod_eq2l q1 aux NS1 q2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)