proposition: Lemma length_c : forall a b n v, length v < length (cons a b n v).
proof: Proof. simpl. intros; apply le_lt_n_Sm. case v. simpl. auto with arith. intros. simpl (length (cons t t0 n0 t1)). simpl (nbterms (cons t t0 n0 t1)). match goal with [ |- ?a <= ?b + ?c + ?d] => rewrite <- (plus_assoc b c d) end. simpl (length_aux (cons t t0 n0 t1)). match goal with [ |- ?a <= ?b + ?c ] => assert (a <= c) end. pattern (max (length t) (max (length t0) (length_aux t1))). generalize (max (length t) (max (length t0) (length_aux t1))). intro n1. simpl. apply le_n_S. apply plus_le_compat_l. repeat rewrite plus_0_r. apply plus_le_compat; apply le_trans with (max (length b) n1); apply le_max_r. omega. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP Gamma0_prelude