proposition: Lemma degenerated_rect_eq : forall A B C, Rectangle A B B C -> A = C.
proof: Proof. intros A B C HRect. apply Rectangle_Parallelogram in HRect; apply plg_mid in HRect. destruct HRect as [M [HMid1 HMid2]]; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates