proposition: Lemma rank_catr x s s' : x \in s -> x \notin s' -> rank x (s ++ s') = size s' + rank x s.
proof: Proof. move=> x_s xNs'; rewrite !rankE rev_cat mem_cat x_s /=. by rewrite index_cat mem_rev (negPf xNs') size_rev. Qed.
imports: mathcomp(all_ssreflect) extra