proposition: Lemma plgf_rect_id : forall A B C D, Parallelogram_flat A B C D -> Rectangle A B C D -> A = D /\ B = C \/ A = B /\ D = C.
proof: Proof. intros. unfold Parallelogram_flat in H. spliter. assert(Per B A D /\ Per A B C /\ Per B C D /\ Per A D C). apply rect_per. assumption. spliter. assert(HH:=l8_9 A B C H6 H). induction HH. right. subst B. apply cong_symmetry in H2. apply cong_identity in H2. subst D. split; reflexivity. left. subst B. apply cong_identity in H3. subst D. split; reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates