proposition: Lemma lexn_eq : forall n (xs ys : prodn n A), lexn eqA gt xs ys <-> (exists i (hi : i<n), gt (projn xs hi) (projn ys hi) /\ forall j, j<i -> forall hj : j<n, eqA (projn xs hj) (projn ys hj)).
proof: Proof. induction n; simpl prodn. intuition. destruct H as [i [hi _]]. lia. intros [x xs] [y ys]. simpl lexn. split; intro h. inversion h; clear h; subst. ex 0 (Nat.lt_0_succ n). split. simpl projn. hyp. intros. lia. rewrite IHn in H4. destruct H4 as [i [hi [h1 h2]]]. ex (S i) (NatCompat.lt_n_S hi). split. simpl. rewrite lt_unique with (h1 := NatCompat.lt_S_n (NatCompat.lt_n_S hi)) (h2:=hi). hyp. intros [|j] k hj; simpl. hyp. apply h2. lia. destruct h as [i [hi [h1 h2]]]. destruct i as [|i]. apply lex1. hyp. apply lex2. gen (h2 _ (Nat.lt_0_succ i) (Nat.lt_0_succ n)). simpl. auto. rewrite IHn. ex i (NatCompat.lt_S_n hi). split. fo. intros j ji jn. gen (h2 _ (NatCompat.lt_n_S ji) (NatCompat.lt_n_S jn)). simpl. rewrite lt_unique with (h1 := NatCompat.lt_S_n (NatCompat.lt_n_S jn)) (h2:=jn). auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)