proposition: Lemma length_a : forall a b n v, length a < length (cons a b n v).
proof: Proof. 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. apply le_plus_trans. apply le_max_l. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP Gamma0_prelude