proposition: Lemma exercise4_5 G H: graph_morph (composeg ^~H) unionb G /\ graph_morph (composeg H) unionb G.
proof: Proof. split. set_extens x. move /compg_P => [px [y ph/setUb_P [z zd JV]]]. apply/setUb_P; aw; ex_tac. rewrite LgV//; apply /compg_P;split => //; ex_tac. move /setUb_P; aw; move => [y ydg]; rewrite LgV//. move /compg_P => [px [t pa pb]]. apply /compg_P;split=> //;ex_tac; union_tac. set_extens x. move /compg_P => [px [y /setUb_P [z zd JV] ph]]. apply/setUb_P; aw; ex_tac; rewrite LgV//; apply /compg_P;split => //; ex_tac. move /setUb_P; aw; move => [y ydg]; rewrite LgV//. move /compg_P => [px [t pa pb]]. apply /compg_P;split => //;ex_tac; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)