proposition: Lemma indexedrP a b c: inc a (indexedr b c) <-> [/\ pairp a, P a = b & inc (Q a) c].
proof: Proof. split; first by move/setX_P => [pa /set1_P pb pc]. move =>[pa pb pc]; apply/setX_P;split => //; rewrite pb;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)