proposition: Lemma gt_trans : forall n m p : nat, n > m -> m > p -> n > p.
proof: Proof. now intros n m p H1 H2; apply Nat.lt_trans with (1 := H2). Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)