proposition: Lemma tc_pr1 X: transitive_closure X = X \cup (unionf X transitive_closure).
proof: Proof. move: (tc_exists X) =>[]. set Y := (transitive_closure X) => pa pb pc. apply: extensionality. set Z := _ \cup _; apply: pc; last by apply:subsetU2l. move => t tz s st; apply /setU2_P; right; apply /setUf_P;case /setU2_P: tz. by move => h;ex_tac; apply:(proj32 (tc_exists t)). by move/setUf_P => [y yx etc]; ex_tac; apply: (proj31 (tc_exists y) _ etc). move => t /setU2_P;case; first by apply: pb. move /setUf_P => [y ya yb]. exact: (proj33 (tc_exists y) Y pa (pa _ (pb _ ya)) _ yb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)