proposition: Lemma tricho_lt_2' : forall a1 a2 b1 b2 n1 n2 r1 r2, length b1 + length (cons a2 b2 0 zero) < length (cons a1 b1 n1 r1) + length (cons a2 b2 n2 r2).
proof: Proof. intros;apply plus_lt_le_compat. apply length_b. simpl. intros; apply le_lt_n_Sm. match goal with [ |- ?a <= ?b + ?c + ?d] => rewrite (plus_comm (b + c) d) end. apply le_plus_trans. replace (Max.max (length b2) 0) with (length b2). generalize (Max.max_dec (length a2) (length b2)). destruct 1. rewrite e. repeat rewrite plus_0_r. apply plus_le_compat. apply le_max_l. apply le_max_l. repeat rewrite plus_0_r. apply plus_le_compat; apply max_le_regL; apply le_max_l. rewrite max_l; auto with arith. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo