proposition: Lemma oprod2_comm4 a b (x := cnf_val a) (y:= cnf_val b): cnfp_nz a -> cnfp_nz b -> \0o <o (oexp a \0c) -> \0o <o oexp b \0c -> oprod_comm x y -> (oprod2_comm_P4 x y \/ oprod2_comm_P4 y x).
proof: Proof. move=> anz bnz tcX tcY cr. move: (cnfp_shift_expo (proj1 anz) (OS_cnf_degree bnz)). move: (cnfp_shift_expo (proj1 bnz) (OS_cnf_degree anz)). set u := cnf_shift_expo _ _. set v := cnf_shift_expo _ _. move => ou ov. have eq2: cnf_val u = cnf_val v. by rewrite -(CNF_prod_pr5 bnz anz tcX) - (CNF_prod_pr5 anz bnz tcY). move:(cnf_val_inj ou ov eq2) => eq3. move: (f_equal domain eq3). rewrite/u/v /cnf_shift_expo !Lgd=> dadb. move:(f_equal (Vg ^~ (cnf_size a)) eq3). move:(cnf_size_nz_bis anz) => pa. have pb: inc (cnf_size a) (domain b) by ue. rewrite/u/v/cnf_shift_expo (LgV pb) (LgV pa) -/(cnf_degree a). rewrite /cnf_size- dadb -/(cnf_size b) -/(cnf_degree b) => /pr1_def csd. move/(osum2_commutes (OS_cnf_degree anz) (OS_cnf_degree bnz)): csd. move => [c [c1 [c2 [oc c1N c2N p1v p2v]]]]. move:(NS_diff c1 c2N) (NS_diff c2 c1N). set c3:= c2 -c c1; set c4:= c1 -c c2 => c3N c4N. move:(OS_nat c1N)(OS_nat c2N) => oc1 oc2. move:(OS_nat c3N)(OS_nat c4N) => oc3 oc4. have disj: ((c1 +c c3 = c2 /\ c4 = \0c) \/ (c2 +c c4 = c1 /\ c3 = \0c)). case: (NleT_ee c1N c2N) => le1. by left; split; [ apply: (cdiff_pr le1) | apply: (cdiff_wrong le1) ]. by right; split; [ apply: (cdiff_pr le1) | apply: (cdiff_wrong le1) ]. have [t [ot tp1 tp2]]: exists t, [/\ ordinalp t, c1 = t +o c4 & c2 = t +o c3]. move:(esym (osum0r oc1))(esym (osum0r oc2)) => sa sb. move:(esym (osum2_2int c1N c3N))(esym (osum2_2int c2N c4N)) => sc sd. by case: disj;move => [<- ->]; [exists c1 | exists c2]; split. move: (p1v); rewrite tp1 (oprodD ot oc4 oc) => p1. move: (p2v); rewrite tp2 (oprodD ot oc3 oc) => p2. have occ3: ordinalp (c *o c3) by fprops. have occ4: ordinalp (c *o c4) by fprops. have sYv: (oopow (c *o c3)) *o x = (oopow (c *o c4)) *o y. rewrite - {1} (CNF_prod_pr0 (proj1 anz) occ3). rewrite - (CNF_prod_pr0 (proj1 bnz) occ4). congr cnf_val. move:eq3; rewrite /u/v/cnf_shift_expo dadb => aux. apply:Lg_exten => i ida. move:(f_equal (Vg ^~ i) aux); rewrite (LgV ida)(LgV ida) => eq4. apply: f_equal2; [symmetry | by rewrite(pr2_def eq4)]. move:(OS_prod2 oc ot) (OS_prod2 oc oc4) (OS_prod2 oc oc3) => o1 o2 o3. move: (proj42 (proj1 anz)) => daN. have lia: i <c domain a by apply/NltP. move:(proj42(proj1(proj44(proj1 anz))) _ lia)=> oa. rewrite - dadb in lia. move:(proj42(proj1(proj44(proj1 bnz))) _ lia)=> ob. move:(pr1_def eq4); rewrite p1 p2. rewrite - {1} (osumA o1 o2 ob) - (osumA o1 o3 oa). by move/(osum2_simpl (OS_sum2 o2 ob) (OS_sum2 o3 oa) o1). case: disj; move=> [pr1 pr2]. left; exists a, c,c1, c3. rewrite sYv pr2 oprod0r oopow0 (oprod1l (OS_cnf_val (proj1 bnz))). by split;last split ;try reflexivity. right; exists b ,c, c2, c4. rewrite - sYv pr2 oprod0r oopow0 (oprod1l (OS_cnf_val (proj1 anz))). by split; last split; try reflexivity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)