proposition: Lemma SN_symprod : forall x, SN gtA x -> forall y, SN gtB y -> SN gt (x,y).
proof: Proof. induction 1 as [x _ IHAcc]; intros y H2. induction H2 as [x1 H3 IHAcc1]. apply SN_intro; intros y H5. inversion_clear H5; auto with sets. apply IHAcc; auto. apply SN_intro; trivial. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)