proposition: Theorem prodRzProp : forall (a b : rZ) (S1 S2 : list rZ), In a S1 -> In b S2 -> In (a, b) (prodRz S1 S2).
proof: Proof. intros a b S1; elim S1; simpl in |- *; auto with stalmarck. intros a0 l H' S2 H'0; Elimc H'0; intros H'0; [ rewrite H'0 | idtac ]; auto with stalmarck. intros H'1; apply in_or_app; auto with stalmarck. left. change (In ((fun b0 : rZ => (a, b0)) b) (map (fun b0 : rZ => (a, b0)) S2)) in |- *. apply in_map; auto with stalmarck. intros H'1; apply in_or_app; auto with stalmarck. Qed.
imports: Coq(List)