proposition: Lemma T3addA c1 c2 c3: c1 + (c2 + c3) = (c1 + c2) + c3.
proof: Proof. elim: c1 c2 c3 => // a1 _ b1 _ c1 _ n1 d1 H; case. by move => c3;rewrite !T3add0n T3addn0. move => a2 b2 c2 n2 s2; case;[ by rewrite !T3addn0 | move => a3 b3 c3 n3 d3 /=]. case: (T3ltgtP [a2, b2, c2] [a3, b3, c3]). + case: (T3ltgtP [a1, b1, c1] [a2, b2, c2]) => pa pb /=. - by rewrite (T3lt_trans pa pb) /= pb. - by case (T3ltgtP a1 a3) => //; rewrite - H /= pb. - by rewrite pa pb. + case: (T3ltgtP [a1, b1, c1] [a2, b2, c2]) => pa pb /=; move: (T3lt_anti pb) => pc. - by rewrite pb pc. - by move:(T3lt_trans pb pa) => h; rewrite h (T3lt_anti h) - H /= pb pc. - by rewrite pa pb pc. + move => e1; case: (T3ltgtP [a1, b1, c1] [a2, b2, c2]) => pb /=; rewrite -e1. - by rewrite !T3ltnn. - by rewrite pb (T3lt_anti pb) - H /= -e1 !T3ltnn. - by rewrite pb !T3ltnn addSn addnS addnA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)