proposition: Lemma cong_trivial_identity : forall A B : Tpoint, Cong A A B B.
proof: Proof. intros. destruct (segment_construction B A B B) as [E [HBet HCong]]. assert(A=E) by (eapply cong_identity;apply HCong). subst. assumption. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish