proposition: Lemma leP_asym : forall O E E' A B, LeP O E E' A B -> LeP O E E' B A -> A = B.
proof: Proof. intros. unfold LeP in *. induction H; induction H0. unfold LtP in *. ex_and H BmA. ex_and H0 AmB. assert(HH:=diff_pos_diff_neg O E E' A B AmB BmA H0 H H2). assert(HT:=diff_pos_diff_neg O E E' B A BmA AmB H H0 H1). apply False_ind. assert(HN:=not_pos_and_neg O E AmB). apply HN. split; auto. auto. auto. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod