proposition: Lemma lt_trans_1 : forall x y z : nat, x < y -> y < S z -> x < z.
proof: Proof. intros x y z H H0. unfold lt in H0. unfold lt in H. unfold lt in |- *. apply le_trans with (m := y). assumption. apply le_S_n. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)