proposition: Lemma T1addA (x y z :T1) : x + (y + z) = (x + y) + z.
proof: Proof. induction x,y,z; only 1-6: easy. - now rewrite !plus_zero_r. - rewrite !plus_cons_cons_eqn. destruct (compare y1 z1) eqn:Hyz, (compare x1 y1) eqn:Hxy; rewrite !plus_cons_cons_eqn. 2,8: now rewrite Hyz, Hxy. all: try compare trans Hxy Hyz as ->. + rewrite Hxy; f_equal; lia. + now rewrite Hxy, <- IHx2, plus_cons_cons_eqn, Hyz. + reflexivity. + now rewrite Hyz. + destruct (compare x1 z1) eqn:?. 1-2: reflexivity. f_equal. rewrite <- IHx2. simpl. now rewrite Hyz. + now rewrite Hxy. + rewrite Hxy, <- IHx2. simpl. now rewrite Hyz. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)