proposition: Lemma StepFSupBall_stable : forall (e : Q) (a b : StepFS (msp_as_RSetoid X)), (~~StepFSupBall e a b) -> StepFSupBall e a b.
proof: Proof. induction a. - induction b. unfold StepFSupBall, StepFfoldProp. simpl. intros. apply (msp_stable (msp X)), H. intros. split. apply IHb1. intro abs. contradict H; intros [H _]. contradiction. apply IHb2. intro abs. contradict H; intros [_ H]. contradiction. - unfold StepFSupBall, StepFfoldProp, Ap. simpl. intros b H. destruct (@Split X b o). split. apply IHa1. intro abs. contradict H; intros [H _]. contradiction. apply IHa2. intro abs. contradict H; intros [_ H]. contradiction. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionSetoid CoRN.metric2.StepFunctionMonad CoRN.metric2.UniformContinuity CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.metric2.Prelength CoRN.algebra.COrdFields2 CoRN.tactics.CornTac