proposition: Lemma concours_unique : forall A B A1 B1 I J : PO, ~ alignes A A1 B -> B1 <> B -> alignes A A1 I -> alignes B1 B I -> alignes A A1 J -> alignes B1 B J -> I = J.
proof: Proof. intros A B A1 B1 I J H. unfold alignes in |- *; intros H50 H0 H1 H2 H3. elim H3; clear H3; [ intros; tauto | unfold alignes1 in |- *; intros ]. elim H1; clear H1; [ intros; tauto | unfold alignes1 in |- *; intros ]. deroule_triangle A A1 B. elim H2; clear H2; [ intros; tauto | unfold alignes1 in |- *; intros ]. elim H0; clear H0 H5 H4; [ intros; tauto; clear H6 | unfold alignes1 in |- *; intros ]. elim H3; intros k0 H4; try clear H3; try exact H4. elim H2; intros k1 H3; try clear H2; try exact H3. elim H1; intros k2 H2; try clear H1; try exact H2. elim H0; intros k3 H1; try clear H0; try exact H1. elim (classic (k0 + - k2 = 0)); intros. cut (k0 = k2); intros. rewrite H5 in H4. apply conversion_PP with (a := 1) (b := 1); auto. rewrite H4; auto. auto with *. cut (cons (k0 + - k2) B = add_PP (cons (k0 * k3 + - (k2 * k1)) A) (cons (k0 + - k2 + - (k0 * k3 + - (k2 * k1))) A1)); intros. assert (~ alignes1 A A1 B); auto with geo. absurd (ex (fun k0 : R => cons 1 B = add_PP (cons k0 A) (cons (1 + - k0) A1))); auto. exists (/ (k0 + - k2) * (k0 * k3 + - (k2 * k1))). apply mult_PP_regulier with (k0 + - k2); auto. pattern 1 at 2 in |- *. replace 1 with ((k0 + - k2) * / (k0 + - k2)); auto. rewrite <- distrib_mult_cons. rewrite def_mult_PP. replace ((k0 + - k2) * (/ (k0 + - k2) * (k0 * k3 + - (k2 * k1)))) with (k0 * k3 + - (k2 * k1)); auto. replace ((k0 + - k2) * 1) with (k0 + - k2); auto. replace ((k0 + - k2) * / (k0 + - k2) + - (/ (k0 + - k2) * (k0 * k3 + - (k2 * k1)))) with (/ (k0 + - k2) * (k0 + - k2 + - (k0 * k3 + - (k2 * k1)))); auto. replace ((k0 + - k2) * (/ (k0 + - k2) * (k0 + - k2 + - (k0 * k3 + - (k2 * k1))))) with (1 * (k0 + - k2 + - (k0 * k3 + - (k2 * k1)))); auto. rewrite H5. RingPP. replace 1 with ((k0 + - k2) * / (k0 + - k2)); auto. ring. auto with *. ring. ring. replace ((k0 + - k2) * (/ (k0 + - k2) * (k0 * k3 + - (k2 * k1)))) with ((k0 + - k2) * / (k0 + - k2) * (k0 * k3 + - (k2 * k1))). replace ((k0 + - k2) * / (k0 + - k2)) with 1. ring. auto with *. ring. auto with *. cut (add_PP (cons (k0 * k2) B1) (cons (k0 * (1 + - k2)) B) = add_PP (cons (k0 * k3) A) (cons (k0 * (1 + - k3)) A1)); intros. cut (add_PP (cons (k2 * k0) B1) (cons (k2 * (1 + - k0)) B) = add_PP (cons (k2 * k1) A) (cons (k2 * (1 + - k1)) A1)); intros. replace (cons (k0 + - k2) B) with (add_PP (cons (k0 * (1 + - k2)) B) (cons (- (k2 * (1 + - k0))) B)). replace (cons (k0 * k3 + - (k2 * k1)) A) with (add_PP (cons (k0 * k3) A) (cons (- (k2 * k1)) A)). replace (cons (k0 + - k2 + - (k0 * k3 + - (k2 * k1))) A1) with (add_PP (cons (k0 * (1 + - k3)) A1) (cons (- (k2 * (1 + - k1))) A1)). RingPP2 H5. cut (add_PP (cons (- (k2 * k0)) B1) (cons (- (k2 * (1 + - k0))) B) = add_PP (cons (- (k2 * k1)) A) (cons (- (k2 * (1 + - k1))) A1)); intros. RingPP2 H8. RingPP. replace (add_PP (cons (- (k2 * k0)) B1) (cons (- (k2 * (1 + - k0))) B)) with (mult_PP (-1) (add_PP (cons (k2 * k0) B1) (cons (k2 * (1 + - k0)) B))). rewrite H7. RingPP. RingPP. RingPP. RingPP. RingPP. rewrite distrib_mult_cons. rewrite distrib_mult_cons. rewrite <- H4. rewrite H3; auto. rewrite distrib_mult_cons. rewrite distrib_mult_cons. rewrite <- H2. rewrite H1; auto. Qed.