proposition: Lemma length_ab : forall a b, length a + length b <= length (cons a b 0 zero).
proof: Proof. simpl. intros. repeat rewrite (max_l (length b) 0);auto with arith. case (le_lt_dec (length a) (length b)). intro;repeat rewrite max_r;auto. omega. intro;repeat rewrite max_l;auto. omega. auto with arith. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP Gamma0_prelude