proposition: Theorem rZltEqComp : forall a b c d : rZ, rZlt a b -> eqRz a c -> eqRz b d -> rZlt c d.
proof: Proof. intros a b c d; unfold rZlt, eqRz in |- *; case a; case b; case c; case d; simpl in |- *; intros a' b' c' d' H'0 H'1 H'2; try rewrite <- H'1; try rewrite <- H'2; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)