proposition: Lemma lt_pred : forall x y : nat, x < y -> x <> 0 -> pred x < pred y.
proof: Proof. simple induction x. intros y H H0. absurd (0 = 0). assumption. reflexivity. intros n H y H0 H1. apply lt_pred. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)