proposition: Lemma exercise6_6c G H: equivalence G -> equivalence H -> substrate G = substrate H -> [/\ sub G (G \cg H), sub H (G \cg H) & forall W, equivalence W -> sub G W -> sub H W -> sub (G \cg H) W].
proof: Proof. move=> eG eH sG. have gg: sgraph G by fprops. have gh: sgraph H by fprops. have gc: sgraph (G \cg H) by apply: compg_graph. split. - move=> y yG. move: (gg _ yG) => py. rewrite - py in yG. apply/ compg_P;split=>//;exists (P y) => //; equiv_tac=>//. rewrite - sG; substr_tac. - move=> y yH. move: (gh _ yH) => py. rewrite - py in yH. apply/compg_P; split=>//;exists (Q y)=>//; equiv_tac=>//. rewrite sG; substr_tac. - move=> w ew gW hW t. move /compg_P=> [tp [y JH JG]]. move: (gW _ JG) (hW _ JH)=> J1G J2G. have: inc (J (P t) (Q t)) w by equiv_tac. by rewrite tp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)