Library GeoCoq.Tarski_dev.Annexes.Tagged_predicates

Require Import GeoCoq.Tarski_dev.Annexes.quadrilaterals.

Section Tagged_predicates.

Context `{Tn:Tarski_neutral_dimensionless}.

Definition Diff_tagged (A B: Tpoint) := A B.

Lemma Diff_Diff_tagged : A B , A B Diff_tagged A B.
Proof.
trivial.
Qed.

Lemma Diff_tagged_Diff : A B , Diff_tagged A B A B.
Proof.
trivial.
Qed.

Lemma Diff_perm :
   (A B: Tpoint),
  A B
  A B B A.
Proof.
intros.
repeat split; intuition.
Qed.

Definition Cong_tagged A B C D := Cong A B C D.

Lemma Cong_Cong_tagged : A B C D, Cong A B C D Cong_tagged A B C D.
Proof.
trivial.
Qed.

Lemma Cong_tagged_Cong : A B C D, Cong_tagged A B C D Cong A B C D.
Proof.
trivial.
Qed.

Definition Bet_tagged A B C := Bet A B C.

Lemma Bet_Bet_tagged : A B C, Bet A B C Bet_tagged A B C.
Proof.
trivial.
Qed.

Lemma Bet_tagged_Bet : A B C, Bet_tagged A B C Bet A B C.
Proof.
trivial.
Qed.

Definition Col_tagged A B C := Col A B C.

Lemma Col_Col_tagged : A B C, Col A B C Col_tagged A B C.
Proof.
trivial.
Qed.

Lemma Col_tagged_Col : A B C, Col_tagged A B C Col A B C.
Proof.
trivial.
Qed.

Definition NCol_tagged A B C := ¬ Col A B C.

Lemma NCol_NCol_tagged : A B C, ¬ Col A B C NCol_tagged A B C.
Proof.
trivial.
Qed.

Lemma NCol_tagged_NCol : A B C, NCol_tagged A B C ¬ Col A B C.
Proof.
trivial.
Qed.

Definition Mid_tagged A B C := Midpoint A B C.

Lemma Mid_Mid_tagged : A B C, Midpoint A B C Mid_tagged A B C.
Proof.
trivial.
Qed.

Lemma Mid_tagged_Mid : A B C, Mid_tagged A B C Midpoint A B C.
Proof.
trivial.
Qed.

Definition Per_tagged A B C := Per A B C.

Lemma Per_Per_tagged : A B C, Per A B C Per_tagged A B C.
Proof.
trivial.
Qed.

Lemma Per_tagged_Per : A B C, Per_tagged A B C Per A B C.
Proof.
trivial.
Qed.

Definition Perp_in_tagged X A B C D := Perp_at X A B C D.

Lemma Perp_in_Perp_in_tagged : X A B C D, Perp_at X A B C D Perp_in_tagged X A B C D.
Proof.
trivial.
Qed.

Lemma Perp_in_tagged_Perp_in : X A B C D, Perp_in_tagged X A B C D Perp_at X A B C D.
Proof.
trivial.
Qed.

Definition Perp_tagged A B C D := Perp A B C D.

Lemma Perp_Perp_tagged : A B C D, Perp A B C D Perp_tagged A B C D.
Proof.
trivial.
Qed.

Lemma Perp_tagged_Perp : A B C D, Perp_tagged A B C D Perp A B C D.
Proof.
trivial.
Qed.

Definition Par_strict_tagged A B C D := Par_strict A B C D.

Lemma Par_strict_Par_strict_tagged : A B C D, Par_strict A B C D Par_strict_tagged A B C D.
Proof.
trivial.
Qed.

Lemma Par_strict_tagged_Par_strict : A B C D, Par_strict_tagged A B C D Par_strict A B C D.
Proof.
trivial.
Qed.

Definition Par_tagged A B C D := Par A B C D.

Lemma Par_Par_tagged : A B C D, Par A B C D Par_tagged A B C D.
Proof.
trivial.
Qed.

Lemma Par_tagged_Par : A B C D, Par_tagged A B C D Par A B C D.
Proof.
trivial.
Qed.

Definition Plg_tagged A B C D := Parallelogram A B C D.

Lemma Plg_Plg_tagged : A B C D, Parallelogram A B C D Plg_tagged A B C D.
Proof.
trivial.
Qed.

Lemma Plg_tagged_Plg : A B C D, Plg_tagged A B C D Parallelogram A B C D.
Proof.
trivial.
Qed.

End Tagged_predicates.