proposition: Lemma iprop_wd : forall I : interval, pred_wd _ I.
proof: Proof. induction I; unfold iprop in |- *; red in |- *; intros x y X X0; try inversion_clear X; try inversion X0. auto. astepr x; auto. astepl x; auto. astepr x; auto. astepl x; auto. split. astepr x; auto. astepl x; auto. split. astepr x; auto. astepl x; auto. split. astepr x; auto. astepl x; auto. split. astepr x; auto. astepl x; auto. Qed.
imports: CoRN.ftc.NthDerivative