proposition: Lemma indexed_P x i y: inc y (x *s1 i) <-> [/\ pairp y, inc (P y) x & Q y = i].
proof: Proof. split; first by move /setX_P => [pa pb /set1_P]. move =>[pa pb <-]; apply: setX_i; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)