MyRelations.v

Require Export Relation_Definitions.
Require Export Relation_Operators.
Require Export Operators_Properties.

Require Export Inclusion.
Require Export Transitive_Closure.
Require Export Union.
Require Export Inverse_Image.
Require Export Lexicographic_Product.

Hints Resolve rt_step rt_refl rst_step rst_refl t_step: core.
Hints Unfold transp union reflexive transitive: core.
Hints Immediate rst_sym : core.

  Lemma clos_refl_trans_ind_right: (A:Set)(R:(relation A))(M:A)(P:A->Prop)
          (P M)
        ->((P0,N:A)(R N P0)->(clos_refl_trans A R P0 M)->(P P0)->(P N))
        ->(a:A)(clos_refl_trans A R a M)->(P a).
Intros.
Generalize H H0 .
(Elim H1; Intros;Auto).
(Apply H4 with y; Auto).

(Apply H3; Intros).
(Apply H5; Intros; Auto).
(Apply H7 with P0; Auto).

(Apply H7 with P0; Auto).
(Apply rt_trans with y; Auto).
Save.

  Hints Resolve left_sym right_sym sp_swap sp_noswap : core.