proposition: Lemma strict_dec_glues : forall a b c F (Hab : a [<=] b) (Hbc : b [<=] c) (Hac : a [<=] c), included (Compact Hac) (Dom F) -> (forall x y, Compact Hab x -> Compact Hab y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) -> (forall x y, Compact Hbc x -> Compact Hbc y -> y[<]x -> forall Hx Hy, F x Hx [<] F y Hy) -> forall x y, Compact Hac x -> Compact Hac 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 Hab Hbc Hac; 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