proposition: Theorem inTripletsComp : forall (L : list triplet) (v : rZ), inTriplets v L -> inTriplets (rZComp v) L.
proof: Proof. intros L; elim L; simpl in |- *; auto with stalmarck. unfold eqRz in |- *; auto with stalmarck. intros v H'; rewrite <- H'; case v; auto with stalmarck. intros a; case a; simpl in |- *; auto with stalmarck. unfold eqRz in |- *; auto with stalmarck. intros H' r r0 r1 l H'0 v H'1; Elimc H'1; intros H'1; [ Elimc H'1; intros H'1; [ rewrite <- H'1 | Elimc H'1; intros H'1; rewrite <- H'1 ] | idtac ]; auto with stalmarck; case v; auto with stalmarck. Qed.