proposition: Lemma enumRNatCorrect : forall (a a1 a2 : nat), a1 <= a2 -> (a1 <= a <= a2 <-> In_ll a (enumRNat (a1,a2))).
proof: Proof. unfold enumRNat. intros a a1 a2. replace (a1, a2).1 with a1 by reflexivity. replace ((a1, a2).2 - a1).+1 with ((a2 - a1).+1) by reflexivity. intros Hleq1. simpl in Hleq1. assert ((a2 - a1).+1 > 0) by ssromega. assert (a2 = ((a2 - a1).+1 - 1) + a1) by ssromega. revert H H0. generalize ((a2 - a1).+1) as n. intros n Hlt Heq. rewrite Heq. clear Heq Hleq1 a2. simpl. revert a1 a. induction n; intros a1 a. - ssromega. - simpl in *. split. + intros Hleq. destruct (Nat.eq_dec a1 a); eauto. right. eapply IHn; ssromega. + intros Hin. destruct Hin. subst. ssromega. destruct n. simpl in *. contradiction. simpl in *. eapply IHn in H; now ssromega. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List