proposition: Theorem allNatsLt_filter_lt : forall (p n : nat), (n <= p)%nat-> filter (fun z => if (lt_dec z n) then true else false) (allNatsLt p) = allNatsLt n.
proof: Proof. induction p; intuition. simpl. assert (n = 0%nat). lia. subst. trivial. simpl. destruct (le_dec n p). rewrite filter_app. rewrite IHp; intuition. simpl. destruct (lt_dec p n ). lia. eapply app_nil_r. assert (n = S p). lia. subst. simpl. rewrite filter_app. f_equal. eapply filter_true. intuition. destruct (lt_dec a (S p)); intuition. apply allNatsLt_lt in H0. lia. simpl. destruct (lt_dec p (S p)); intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation