proposition: Lemma Exercise3_1b E F f g: function_prop f E F -> function_prop g F E -> injection g -> exists A A', [/\ sub A E, sub A' F, Vfs f A = A' & Vfs g (F -s A') = E -s A].
proof: Proof. move=> fp1 fp2 ig; move: (Exercise3_1 fp2 fp1 ig). move=> [A0 [A1 [pa pb pc pd]]]. exists (E -s A1); exists (F -s A0). split => //; try apply: sub_setC; rewrite !setC_K //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)