proposition: Lemma rept_union_inc x y: inc y x -> forall n, natp n -> sub (rept_union y n) (rept_union x (csucc n)).
proof: Proof. move: (rept_union_pr y) => [sc sd] yx. move: (rept_union_pr x) => [sa sb]. apply:Nat_induction. by rewrite sc (sb _ NS0) sa; apply: setU_s1. move => n nN Hrec. rewrite (sd _ nN) (sb _ (NS_succ nN)). move => t /setU_P [z tz /Hrec etc]; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)