GeoCoq in the browser

Require Export GeoCoq.Tarski_dev.Annexes.midpoint_theorems. Section Logic. Lemma example_0 : forall A B C : Prop, (A -> B) -> (B -> C) -> (A -> C). Proof. Admitted. Lemma example_1 : forall A B C : Prop, (A /\ B -> C) <-> (A -> B -> C). Proof. Admitted. Lemma example_2 : forall A B : Prop, A \/ B -> B \/ A. Proof. Admitted. End Logic. Section Varignon. Context `{TE:Tarski_euclidean}. Check cong3_conga. Definition isosceles A B C := Cong A B B C. Lemma isosceles_conga : forall A B C, A<>C -> A<>B -> isosceles A B C -> CongA C A B A C B. Proof. Admitted. (** This is the usual proof presented in classroom based on the midpoint theorem but this proof suffers from two problems. It needs the fact that IJK are not collinear, which is not always the case when the quadrilateral is not convex. It also needs the fact that A is different from C, and B is different from D. The original proof by Varignon suffer from the same problem. The original proof can be found page 138, Corollary IV: http://polib.univ-lille3.fr/documents/B590092101_000000011.489_IMT.pdf *) Lemma varignon : forall A B C D I J K L, A<>C -> B<>D -> ~ Col I J K -> Midpoint I A B -> Midpoint J B C -> Midpoint K C D -> Midpoint L A D -> Parallelogram I J K L. Proof. intros. (* assert_diffs. bugged *) assert (I <> J) by (intro; subst; Col). assert (I <> K) by (intro; subst; Col). assert (J <> K) by (intro; subst; Col). assert (Par I L B D) (** Applying the midpoint theorem in the triangle BDA. *) by perm_apply (triangle_mid_par B D A L I). assert (Par J K B D) (** Applying the midpoint theorem in the triangle BDC. *) by perm_apply (triangle_mid_par B D C K J). assert (Par I L J K) (** Transitivity of parallelism *) by (apply par_trans with B D;finish). assert (Par I J A C) (** Applying the midpoint theorem in the triangle ACB. *) by perm_apply (triangle_mid_par A C B J I). assert (Par L K A C) (** Applying the midpoint theorem in the triangle ACD. *) by perm_apply (triangle_mid_par A C D K L). assert (Par I J K L) (** Transitivity of parallelism *) by (apply par_trans with A C;finish). apply par_2_plg;finish. (** If in the opposite side of quadrilatral are parallel and two opposite side are distinct then it is a parallelogram. *) Qed. End Varignon.