proposition: Theorem prodRzInL : forall (a b : rZ) (L1 L2 : list rZ), In (a, b) (prodRz L1 L2) -> In a L1.
proof: Proof. intros a b L1; elim L1; simpl in |- *; auto with stalmarck. intros a0 l H' L2 H'0. case (in_app_or _ _ _ H'0); auto with stalmarck. elim L2; simpl in |- *; auto with stalmarck. intros H'1; elim H'1; auto with stalmarck. intros a1 l0 H'1 H'2; Elimc H'2; intros H'2; [ inversion H'2 | idtac ]; auto with stalmarck. intros H'1; right; auto with stalmarck. apply H' with (L2 := L2); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)