proposition: Lemma doubleI_rgP f a b x: inc x (doubleI_rg f a b) <-> ((exists2 y, inc y b & x = f a y) \/ (exists2 y, inc y a & x = f y b)).
proof: Proof. split. case/setU2_P => /funI_P [z zab ->]; [ right; ex_tac | left; ex_tac]. by case => - [y yb ->]; apply/setU2_P; [right | left ]; apply: funI_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)