proposition: Theorem inTripletsCompInv : forall (L : list triplet) (v : rZ), inTriplets (rZComp v) L -> inTriplets v L.
proof: Proof. intros L v H'; rewrite (rZCompInvol v). apply inTripletsComp; auto with stalmarck. Qed.