proposition: Theorem rVltrZComp : forall (a : rZ) (b : rNat), rVlt a b -> rVlt (rZComp a) b.
proof: Proof. intros a b; case a; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)