proposition: Lemma length_c : forall a b n v, t2_length v < t2_length (gcons a b n v).
proof: Proof. simpl; intros; apply Compat815.le_lt_n_Sm; case v. - simpl; lia. - intros; simpl (t2_length (gcons t t0 n0 t1)). simpl (nbterms (gcons t t0 n0 t1)). match goal with [ |- ?a <= ?b + ?c + ?d] => rewrite <- (Nat.add_assoc b c d) end. simpl (t2_length_aux (gcons t t0 n0 t1)). match goal with [ |- ?a <= ?b + ?c ] => assert (a <= c) end. { pattern (Nat.max (t2_length t) (Nat.max (t2_length t0) (t2_length_aux t1))). generalize (Nat.max (t2_length t) (Nat.max (t2_length t0) (t2_length_aux t1))). intro n1; simpl; lia. } abstract lia. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)