proposition: Lemma Acc_symprod : forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y).
proof: Proof. induction 1 as [x _ IHAcc]; intros y H2. induction H2 as [x1 H3 IHAcc1]. apply Acc_intro; intros y H5. inversion_clear H5; auto with sets. apply IHAcc; auto. apply Acc_intro; trivial. Defined.
imports: EqdepFacts Relation_Operators Transitive_Closure Inclusion Inverse_Image