proposition: Lemma no_rep_flat_map_seq2 : forall {A: Type} (f : nat -> list A) len n ka kb, no_repeats (flat_map f (seq n len)) -> LIn ka (seq n len) -> LIn kb (seq n len) -> ka <> kb -> disjoint (f ka) (f kb).
proof: Proof. intros ? ? ? ? ? ? H1 Hb Hc Heq. pose proof (lt_eq_lt_dec ka kb) as Hd. dorn Hd;[dorn Hd|]; subst; cpx. apply LInSeqIff in Hc; repnd. destruct (@no_rep_flat_map_seq1 A f len n ka H1 Hb) as [? dd]. apply dd; cpx. apply LInSeqIff in Hb; repnd. destruct (@no_rep_flat_map_seq1 A f len n kb H1 Hc) as [? dd]. apply disjoint_sym. apply dd; cpx. Qed.
imports: UsefulTypes bin_rels Omega