proposition: Theorem length_compute_lt_O : forall t, 0 < length (compute_code t).
proof: Proof. intros t; elim t; simpl in |- *; auto with arith. intros b H b0 H0; rewrite app_length. replace 0 with (0 + 0); auto with arith. apply Nat.add_lt_mono. generalize H; elim (compute_code b); simpl in |- *; auto with arith. generalize H0; elim (compute_code b0); simpl in |- *; auto with arith. Qed.
imports: Coq(ArithRing ListDec)