proposition: Lemma lea_refl : forall A B C, A <> B -> C <> B -> LeA A B C A B C.
proof: Proof. intros. unfold LeA. exists C . split. apply inangle3123; assumption. apply conga_refl; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2