proposition: Lemma conga_right_comm : forall A B C D E F, CongA A B C D E F -> CongA A B C F E D.
proof: Proof. intros. apply conga_trans with D E F. apply H. unfold CongA in H. spliter. apply conga_pseudo_refl;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2