proposition: Lemma length_ab : forall a b, t2_length a + t2_length b <= t2_length (gcons a b 0 zero).
proof: Proof. simpl; intros. repeat rewrite (max_l (t2_length b) 0);auto with arith. case (le_lt_dec (t2_length a) (t2_length b)). - intro;repeat rewrite max_r;auto. abstract lia. - intro;repeat rewrite max_l;auto. abstract lia. auto with arith. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)