proposition: Lemma lam_perm : forall A B C D, Lambert A B C D -> Lambert A D C B.
proof: Proof. intros. unfold Lambert in *. spliter. repeat split; Perp; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma