proposition: Lemma strict_dec_glues' : forall a b c F, a [<] b -> b [<] c -> included (olor a c) (Dom F) -> (forall x y, olcr a b x -> olcr a b y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) -> (forall x y, clor b c x -> clor b c y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) -> forall x y, olor a c x -> olor a c y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy.
proof: Proof. intros. apply inv_cancel_less. astepl ( {--}F y Hy); astepr ( {--}F x Hx). apply strict_inc_glues' with a b c; auto. intros; simpl in |- *; apply inv_resp_less; auto. intros; simpl in |- *; apply inv_resp_less; auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3