proposition: Lemma length_abnc : forall a b n c, length a + length b <= length (cons a b n c).
proof: Proof. intros. eapply Le.le_trans. eapply length_ab. apply length_psi. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP Gamma0_prelude