proposition: Lemma chain_related_re x: inc x E <-> chain_related x x.
proof: Proof. split. by move=> xE; exists (chain_pair x x);split => //; apply /A1. case; case => a b [h <- _]; [by apply: (A3 h) | by case:h => /A3 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)