proposition: Lemma RhombusExABC1: forall A B C, A <> C -> Col A B C -> Cong A B B C -> exists D, Rhombus A B C D.
proof: Proof. intros. assert(Midpoint B A C). apply ColCongMid; tauto. exists B. unfold Rhombus in *. split. unfold Plg in *. split. tauto. exists B. split. assumption. Midpoint. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.perp_bisect