proposition: Lemma T1addA c1 c2 c3: c1 + (c2 + c3) = (c1 + c2) + c3.
proof: Proof. elim: c1 c2 c3 => // a1 _ n1 b1 H; case. by move => c3;rewrite !T1add0n T1addn0. move => a2 n2 b2; case;[ by rewrite ! T1addn0 | move => a3 n3 b3 /=]. case (T1ltgtP a2 a3). + case (T1ltgtP a1 a2) => pa pb /=. - by rewrite (T1lt_trans pa pb) /= pb. - by case (T1ltgtP a1 a3) => //; rewrite - H /= pb. - by rewrite pa pb. + case (T1ltgtP a1 a2) => pa pb /=; move: (T1lt_anti pb) => pc. - by rewrite pb pc. - by move:(T1lt_trans pb pa) => h; rewrite h (T1lt_anti h) - H /= pb pc. - by rewrite pa pb pc. + move => <-; case (T1ltgtP a1 a2) => pb /=. - by rewrite !T1ltnn. - by rewrite pb (T1lt_anti pb) - H /= !T1ltnn. - by rewrite pb !T1ltnn addSn addnS addnA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)