proposition: Lemma olor_pos_clcr_nonneg : forall a b (F : PartIR), a [<] b -> (forall x, olor a b x -> forall Hx, [0] [<] F x Hx) -> forall Ha, [0] [<=] F a Ha -> forall Hb, [0] [<=] F b Hb -> forall x, clcr a b x -> forall Hx, [0] [<=] F x Hx.
proof: Proof. intros a b F Hab H Ha H0 Hb H1 x H2 Hx. rewrite -> leEq_def; intros H3. cut (Not (olor a b x)); intro H4. elim (less_cotransitive_unfolded _ _ _ Hab x); intro H5. cut (x [=] b). intro H6. rewrite -> leEq_def in H1; apply H1. eapply less_wdl; [ apply H3 | algebra ]. red in H4. apply not_ap_imp_eq; intro H6. inversion_clear H2. elim (ap_imp_less _ _ _ H6); intros. apply H4; split; auto. apply (less_irreflexive_unfolded _ b); apply less_leEq_trans with x; auto. cut (x [=] a); intros. rewrite -> leEq_def in H0; apply H0. eapply less_wdl; [ apply H3 | algebra ]. red in H4. apply not_ap_imp_eq; intro. inversion_clear H2. elim (ap_imp_less _ _ _ X); intros. apply (less_irreflexive_unfolded _ a); apply leEq_less_trans with x; auto. apply H4; split; auto. apply (less_irreflexive_unfolded IR [0]); apply less_transitive_unfolded with (F x Hx); auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3