proposition: Lemma length_n : forall a b r n p, n < p -> length (cons a b n r) < length (cons a b p r).
proof: Proof. induction 1. simpl. auto with arith. simpl;auto with arith. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP Gamma0_prelude