proposition: Lemma lex_SN : forall a, SN gtA a -> forall b, SN gtB b -> SN lex (a, b).
proof: Proof. induction 1 as [a Ha1 Ha2]. induction 1 as [b Hb1 Hb2]. apply SN_intro. destruct y as (a'',b'). intro H. inversion H; subst a'' b'0 a0 b0. apply Ha2. exact H1. apply WF_gtB. apply (@lex_SN_eq a). 2: exact H3. apply Hb2. exact H5. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)