proposition: Lemma iso_rec_dir_distinct : forall A B C : PO, isocele_rectangle_direct A B C -> A <> C.
proof: Proof. unfold isocele_rectangle_direct, isocele in |- *; intros. elim H; [ intros H0 H1; elim H1; [ intros H2 H3; try clear H1 H; try exact H2 ] ]. apply isometrie_distinct with (2 := H2); auto. Qed.