proposition: Lemma gpred_lt : forall (N0 : nat) (c : T1) (H:correct (S (S N0)) c) (H': nf c), match (gpred N0 c H H') with (exist c' _) => c = zero /\ c'=zero \/ c' < c end.
proof: Proof. intros. case (gpred N0 c H H');simpl. intros x Hx; case Hx. destruct 2;auto. Qed.
imports: More_nat Arith ArithRing EPSILON0