proposition: Lemma olor_pos_clor_nonneg : forall a b (F : PartIR), (forall x, olor a b x -> forall Hx, [0] [<] F x Hx) -> forall Ha, [0] [<=] F a Ha -> forall x, clor a b x -> forall Hx, [0] [<=] F x Hx.
proof: Proof. intros a b F H Ha H0 x H1 Hx. rewrite -> leEq_def; intros H2. cut (Not (olor a b x)); intro H3. cut (x [=] a). intro H4. rewrite -> leEq_def in H0; apply H0. eapply less_wdl; [ apply H2 | algebra ]. red in H3. apply not_ap_imp_eq; intro H4. inversion_clear H1. elim (ap_imp_less _ _ _ H4); intros. apply (less_irreflexive_unfolded _ a); apply leEq_less_trans with x; auto. apply H3; 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