proposition: Lemma exercise6_11b1 E X: exercise6_11b_assumption X E -> reflexive_re (exercise6_11b_rel X) E.
proof: Proof. move=> [h _] x; rewrite /exercise6_11b_rel -h;split. move => xE; move: (setU_hi xE)=> [y ye xy];ex_tac. move=> [y [yX xy _ ]]; apply: (setU_i xy yX). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)