proposition: Lemma seq_last_mono (s1 s2 : seq A) leT x : transitive leT -> path leT x s1 -> path leT x s2 -> {subset s1 <= s2} -> (last x s1 == last x s2) || leT (last x s1) (last x s2).
proof: Proof. move=>T; case: s1=>/= [_ H1 _|a s]; first by apply: path_last H1. case/andP=>H1 H2 H3 H; apply: sorted_last_key_max (path_sorted H3) _=>//. apply: {x s2 H1 H3} H; rewrite inE orbC -implyNb. by case E: (_ \notin _) (@seq_last_in s a)=>//= ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)