proposition: Lemma rept_union_inc2 x y n: natp n -> inc y (rept_union x (csucc n)) -> exists2 z, inc z x & inc y (rept_union z n).
proof: Proof. move => nN; rewrite (proj2 (rept_union_pr x) _ nN). move: n nN x y;apply: Nat_induction. move => x y; rewrite (proj1 (rept_union_pr x)) => /setU_P [z yz zx];ex_tac. by rewrite (proj1(rept_union_pr z)). move => n nN Hrec x y. rewrite (proj2 (rept_union_pr x) n nN) => /setU_P [z yz /Hrec [t tx zu]]. ex_tac; rewrite (proj2 (rept_union_pr t) n nN); union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)