proposition: Lemma prop_34_1 : forall A B D C, A <> B /\ A <> D /\ B <> D -> Parallelogram A B D C -> (CongA A B D D C A /\ CongA B D C C A B) /\ (Cong A B D C /\ Cong A C B D).
proof: Proof. intros; split. - apply plg_conga; auto. - apply plg_cong; auto. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions