proposition: Lemma induced_rel_relatedP u v: related (induced_relation r a) u v <-> [/\ inc u a, inc v a & related r u v].
proof: Proof. move: (induced_rel_iirel_axioms) => iia. move: ira=> [er ar]. split. move/(iirel_relatedP iia); rewrite lf_source; move => [pa pb]. rewrite ci_V //ci_V //. move => [ua va ruv];apply/(iirel_relatedP iia); rewrite lf_source; split => //. rewrite ci_V //ci_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)