proposition: Lemma seq_last_monoR (s1 s2 : seq A) leT x : reflexive leT -> transitive leT -> path leT x s1 -> path leT x s2 -> {subset s1 <= s2} -> leT (last x s1) (last x s2).
proof: Proof. by move=>R T P1 P2 S; case: eqP (seq_last_mono T P1 P2 S)=>[->|]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)