proposition: Lemma NoDupNumUpTo : forall n l, NoDup l -> (forall n', In n' l -> S n' > n) -> NoDup (NumUpTo n l).
proof: Proof. induction n. - simpl; eauto. - simpl; intros. eapply IHn. + constructor; eauto. intro H'; apply H0 in H'; eapply Gt.gt_irrefl; eauto. + intros; destruct H1; subst. eauto with arith. apply H0 in H1; eauto with arith. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Numbers.Natural.Peano.NPeano Coq.Strings.String Coq.Arith.Lt Coq.Arith.Compare_dec Coq.Lists.List Coq.ZArith.ZArith