proposition: Lemma strict_inc_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 -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) -> (forall x y, clor b c x -> clor b c y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) -> forall x y, olor a c x -> olor a c y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy.
proof: Proof. intros a b c F Hab Hbc H H0 H1 x y H2 H3 H4 Hx Hy. cut (Dom F b); [ intro Hb | apply H; split; auto ]. elim (less_cotransitive_unfolded _ _ _ H4 b); intro. cut (Dom F (Min b y)); [ intro H5 | apply H; split ]. 2: apply less_Min; auto; elim H3; auto. 2: eapply leEq_less_trans; [ apply Min_leEq_lft | auto ]. apply less_leEq_trans with (F _ H5). cut (Dom F (Min ((x[+]b) [/]TwoNZ) y)); [ intro Hxy | apply H; split ]. 3: elim H3; intros; eapply leEq_less_trans; [ apply Min_leEq_rht | auto ]. 2: apply less_Min. 3: elim H3; auto. 2: apply shift_less_div; [ apply pos_two | rstepl (a[+]a) ]. 2: apply plus_resp_less_both; elim H2; auto. apply less_leEq_trans with (F _ Hxy). apply H0; try split. elim H2; auto. apply less_leEq; auto. apply less_Min. 2: elim H3; auto. apply shift_less_div; [ apply pos_two | rstepl (a[+]a) ]. apply plus_resp_less_both; elim H2; auto. eapply leEq_transitive. apply Min_leEq_lft. apply shift_div_leEq; [ apply pos_two | rstepr (b[+]b) ]. apply plus_resp_leEq; apply less_leEq; auto. apply less_Min; auto. apply shift_less_div; [ apply pos_two | rstepl (x[+]x) ]. apply plus_resp_leEq_less; [ apply leEq_reflexive | auto ]. apply part_mon_imp_mon' with (iprop (olcr a b)); auto. intros x0 H6; apply H; inversion_clear H6; split; auto. apply leEq_less_trans with b; auto. split. apply less_Min. apply shift_less_div; [ apply pos_two | rstepl (a[+]a) ]. apply plus_resp_less_both; auto; elim H2; auto. elim H3; auto. eapply leEq_transitive. apply Min_leEq_lft. apply shift_div_leEq; [ apply pos_two | rstepr (b[+]b) ]. apply plus_resp_leEq; apply less_leEq; auto. split. apply less_Min; auto; elim H3; auto. apply Min_leEq_lft. apply leEq_Min. eapply leEq_transitive. apply Min_leEq_lft. apply shift_div_leEq; [ apply pos_two | rstepr (b[+]b) ]. apply plus_resp_leEq; apply less_leEq; auto. apply Min_leEq_rht. rewrite -> leEq_def; intro H6. cut (y [<=] b); rewrite -> leEq_def; intro H7. apply (less_irreflexive_unfolded _ (F y Hy)). eapply less_wdr. apply H6. apply pfwdef; eapply eq_transitive_unfolded. apply Min_comm. apply leEq_imp_Min_is_lft; rewrite -> leEq_def; auto. apply (less_irreflexive_unfolded _ (F y Hy)). eapply less_transitive_unfolded. apply H6. apply less_wdl with (F b Hb). 2: apply pfwdef; apply eq_symmetric_unfolded; apply leEq_imp_Min_is_lft; apply less_leEq; auto. apply H1; auto. split; auto; apply leEq_reflexive. split; [ apply less_leEq | elim H3 ]; auto. cut (Dom F (Max b x)); [ intro H5 | apply H; split ]. 3: apply Max_less; auto; elim H2; auto. 2: eapply less_leEq_trans; [ apply Hab | apply lft_leEq_Max ]. apply leEq_less_trans with (F _ H5). 2: cut (Dom F (Max ((y[+]b) [/]TwoNZ) x)); [ intro Hxy | apply H; split ]. 3: elim H2; intros; eapply less_leEq_trans; [ apply a0 | apply rht_leEq_Max ]. 3: apply Max_less. 4: elim H2; auto. 3: apply shift_div_less; [ apply pos_two | rstepr (c[+]c) ]. 3: apply plus_resp_less_both; elim H3; auto. 2: apply leEq_less_trans with (F _ Hxy). 3: apply H1; try split. 6: elim H3; auto. 5: apply less_leEq; auto. 4: apply Max_less. 5: elim H2; auto. 4: apply shift_div_less; [ apply pos_two | rstepr (c[+]c) ]. 4: apply plus_resp_less_both; elim H3; auto. 3: eapply leEq_transitive. 4: apply lft_leEq_Max. 3: apply shift_leEq_div; [ apply pos_two | rstepl (b[+]b) ]. 3: apply plus_resp_leEq; apply less_leEq; auto. 3: apply Max_less; auto. 3: apply shift_div_less; [ apply pos_two | rstepr (y[+]y) ]. 3: apply plus_resp_less_lft; auto. 2: apply part_mon_imp_mon' with (iprop (clor b c)); auto. 2: intros x0 H6; apply H; inversion_clear H6; split; auto. 2: apply less_leEq_trans with b; auto. 3: split. 4: apply Max_less. 4: apply shift_div_less; [ apply pos_two | rstepr (c[+]c) ]. 4: apply plus_resp_less_both; auto; elim H3; auto. 4: elim H2; auto. 3: eapply leEq_transitive. 4: apply lft_leEq_Max. 3: apply shift_leEq_div; [ apply pos_two | rstepl (b[+]b) ]. 3: apply plus_resp_leEq; apply less_leEq; auto. 2: split. 3: apply Max_less; auto; elim H2; auto. 2: apply lft_leEq_Max. 2: apply Max_leEq. 2: eapply leEq_transitive. 3: apply lft_leEq_Max. 2: apply shift_leEq_div; [ apply pos_two | rstepl (b[+]b) ]. 2: apply plus_resp_leEq; apply less_leEq; auto. 2: apply rht_leEq_Max. rewrite -> leEq_def; intro H6. cut (b [<=] x); rewrite -> leEq_def; intro H7. apply (less_irreflexive_unfolded _ (F x Hx)). eapply less_wdl. apply H6. apply pfwdef; apply leEq_imp_Max_is_rht; rewrite -> leEq_def; auto. apply (less_irreflexive_unfolded _ (F x Hx)). eapply less_transitive_unfolded. 2: apply H6. apply less_wdr with (F b Hb). 2: apply pfwdef; apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply Max_comm. 2: apply leEq_imp_Max_is_rht; apply less_leEq; auto. apply H0; auto. split; [ elim H2 | apply less_leEq ]; auto. split; auto; apply leEq_reflexive. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3