proposition: Lemma exercise6_10_b r E: reflexive_re r E -> reflexive_re (fun x y => r x y /\ r y x) E.
proof: Proof. move => rr y; split; [by move/rr | by case; move /rr]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)