Set Implicit Arguments.
Unset Strict Implicit.
Require Export point_angle.
 
Lemma calcul4 :
 forall a b c d : AV,
 R (plus (plus a b) (plus c d)) (plus (plus a c) (plus b d)).
(* Goal: forall a b c d : AV, R (plus (plus a (plus b c)) (plus d d)) (plus a (plus (plus d b) (plus d c))) *)
intros a b c d; try assumption.
(* Goal: R (plus (plus a b) (plus c d)) (plus (plus a c) (plus b d)) *)
apply transitive with (plus (plus (plus a b) c) d); auto.
(* Goal: R (plus (plus (plus a b) c) d) (plus (plus a c) (plus b d)) *)
apply transitive with (plus (plus (plus a c) b) d); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (plus a b) c) (plus (plus a c) b) *)
apply transitive with (plus a (plus b c)); auto.
(* Goal: R (plus a (plus b c)) (plus (plus a c) b) *)
apply transitive with (plus a (plus c b)); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
Qed.
 
Theorem angle_inscrit :
 forall A B M O : PO,
 isocele O M A ->
 isocele O M B ->
 R (double (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)).
(* Goal: forall (A B M O : PO) (_ : isocele O M A) (_ : isocele O M B), R (double (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
intros A B M O H H0; try assumption.
(* Goal: R (double (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
unfold double in |- *.
(* Goal: R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
lapply (triangle_isocele (A:=O) (B:=M) (C:=B)); intros.
(* Goal: R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: isocele O M B *)
lapply (isocele_permute (A:=O) (B:=M) (C:=A)); intros.
cut
 (R
    (plus (cons (vec O A) (vec O B))
       (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))))
    (plus pi pi)).
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
intros.
apply
 transitive
  with
    (plus
       (plus (cons (vec O A) (vec O B))
          (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))))
       (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))).
apply
 transitive
  with
    (plus zero (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))).
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
(* Goal: R (plus zero zero) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply zero_plus_a.
apply
 transitive
  with
    (plus (plus pi pi)
       (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))).
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
(* Goal: R (plus pi pi) zero *)
(* Goal: R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) *)
(* Goal: R (plus (plus pi pi) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) (plus (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply pi_plus_pi.
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply reflexive.
apply
 transitive
  with
    (plus (plus pi pi)
       (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))).
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply reflexive.
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply reflexive.
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
try exact H3.
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply reflexive.
apply
 transitive
  with
    (plus (cons (vec O A) (vec O B))
       (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))
          (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))))).
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))))) (plus (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply point_angle.plus_assoc.
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply transitive with (plus (cons (vec O A) (vec O B)) zero).
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply reflexive.
apply
 transitive
  with
    (plus (plus (cons (vec M B) (vec M A)) (cons (vec M A) (vec M B)))
       (plus (cons (vec M B) (vec M A)) (cons (vec M A) (vec M B)))).
(* Goal: R (plus (plus b c) (plus d d)) (plus (plus b d) (plus c d)) *)
(* Goal: R (plus (plus b d) (plus c d)) (plus (plus d b) (plus d c)) *)
apply calcul4.
(* Goal: R (plus (plus (cons (vec M B) (vec M A)) (cons (vec M A) (vec M B))) (plus (cons (vec M B) (vec M A)) (cons (vec M A) (vec M B)))) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply transitive with (plus zero zero).
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: R (plus (cons (vec M B) (vec M A)) (cons (vec M A) (vec M B))) zero *)
(* Goal: R (plus zero zero) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply permute.
(* Goal: R (plus (cons (vec M B) (vec M A)) (cons (vec M A) (vec M B))) zero *)
(* Goal: R (plus zero zero) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply permute.
(* Goal: R (plus zero zero) zero *)
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply zero_plus_a.
(* Goal: R (plus (cons (vec O A) (vec O B)) zero) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply plus_zero.
apply
 transitive
  with
    (plus (plus (cons (vec O A) (vec O M)) (cons (vec O M) (vec O B)))
       (plus (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O)))
          (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))))).
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
(* Goal: R (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))) (cons (vec M B) (vec M A)) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (cons (vec O M) (vec O B))) (plus (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply Chasles.
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
apply
 transitive with (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))).
(* Goal: R (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))) *)
(* Goal: R (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))) (cons (vec M B) (vec M A)) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (cons (vec O M) (vec O B))) (plus (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply plus_sym.
(* Goal: R (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))) (cons (vec M B) (vec M A)) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (cons (vec O M) (vec O B))) (plus (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply Chasles.
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
apply
 transitive with (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))).
(* Goal: R (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))) *)
(* Goal: R (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))) (cons (vec M B) (vec M A)) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (cons (vec O M) (vec O B))) (plus (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply plus_sym.
(* Goal: R (plus (cons (vec M B) (vec M O)) (cons (vec M O) (vec M A))) (cons (vec M B) (vec M A)) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (cons (vec O M) (vec O B))) (plus (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply Chasles.
apply
 transitive
  with
    (plus
       (plus (cons (vec O A) (vec O M))
          (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A))))
       (plus (cons (vec O M) (vec O B))
          (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))).
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus (plus (cons (vec O A) (vec O M)) (cons (vec O M) (vec O B))) (plus (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))) (plus (cons (vec M O) (vec M A)) (cons (vec M B) (vec M O))))) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply calcul3.
(* Goal: R (plus (plus (cons (vec O A) (vec O M)) (plus (cons (vec M O) (vec M A)) (cons (vec M O) (vec M A)))) (plus (cons (vec O M) (vec O B)) (plus (cons (vec M B) (vec M O)) (cons (vec M B) (vec M O))))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
apply compatible.
(* Goal: circonscrit M A B O *)
(* Goal: and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
try exact H2.
(* Goal: R (cons (vec O A) (vec O B)) pi *)
try exact H1.
(* Goal: not (colineaire (vec M A) (vec M B)) *)
try exact H.
(* Goal: isocele O M B *)
try exact H0.
Qed.
 
Lemma triangle_rectangle :
 forall A B M O : PO,
 isocele O M A ->
 isocele O M B ->
 orthogonal (vec M A) (vec M B) -> R (cons (vec O A) (vec O B)) pi.
(* Goal: forall (A B M O : PO) (_ : isocele O M A) (_ : isocele O M B) (_ : R (cons (vec O A) (vec O B)) pi), orthogonal (vec M A) (vec M B) *)
unfold orthogonal in |- *.
(* Goal: forall (A B M O : PO) (_ : isocele O M A) (_ : isocele O M B) (_ : R (cons (vec O A) (vec O B)) pi), R (double (cons (vec M A) (vec M B))) pi *)
intros A B M O H H0 H1; try assumption.
(* Goal: R (cons (vec O A) (vec O B)) pi *)
apply transitive with (double (cons (vec M A) (vec M B))).
(* Goal: R (cons (vec O A) (vec O B)) (double (cons (vec M A) (vec M B))) *)
(* Goal: R (double (cons (vec M A) (vec M B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply symetrique; apply angle_inscrit; auto.
(* Goal: R (cons (vec O A) (vec O B)) pi *)
try exact H1.
Qed.
 
Lemma triangle_diametre :
 forall A B M O : PO,
 isocele O M A ->
 isocele O M B ->
 R (cons (vec O A) (vec O B)) pi -> orthogonal (vec M A) (vec M B).
(* Goal: forall (A B M O : PO) (_ : isocele O M A) (_ : isocele O M B) (_ : R (cons (vec O A) (vec O B)) pi), orthogonal (vec M A) (vec M B) *)
unfold orthogonal in |- *.
(* Goal: forall (A B M O : PO) (_ : isocele O M A) (_ : isocele O M B) (_ : R (cons (vec O A) (vec O B)) pi), R (double (cons (vec M A) (vec M B))) pi *)
intros A B M O H H0 H1; try assumption.
(* Goal: R (double (cons (vec M' A) (vec M' B))) (double (cons (vec M A) (vec M B))) *)
apply transitive with (cons (vec O A) (vec O B)).
(* Goal: R (double (cons (vec M' A) (vec M' B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply angle_inscrit; auto.
(* Goal: R (cons (vec O A) (vec O B)) pi *)
try exact H1.
Qed.
 
Theorem cocyclique :
 forall M A B O M' : PO,
 isocele O A B ->
 isocele O M A ->
 isocele O M B ->
 isocele O M' A ->
 isocele O M' B ->
 R (double (cons (vec M' A) (vec M' B))) (double (cons (vec M A) (vec M B))).
(* Goal: forall (M A B O M' : PO) (_ : isocele O A B) (_ : isocele O M A) (_ : isocele O M B) (_ : isocele O M' A) (_ : isocele O M' B), R (double (cons (vec M' A) (vec M' B))) (double (cons (vec M A) (vec M B))) *)
intros M A B O M' H H0 H1 H2 H3; try assumption.
(* Goal: R (double (cons (vec M' A) (vec M' B))) (double (cons (vec M A) (vec M B))) *)
apply transitive with (cons (vec O A) (vec O B)).
(* Goal: R (double (cons (vec M' A) (vec M' B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply angle_inscrit; auto.
(* Goal: R (cons (vec O A) (vec O B)) (double (cons (vec M A) (vec M B))) *)
(* Goal: R (double (cons (vec M A) (vec M B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply symetrique; apply angle_inscrit; auto.
Qed.
 
Lemma exists_opp_angle : forall a : AV, exists b : AV, R (plus a b) zero.
(* Goal: not (colineaire (vec M A) (vec M B)) *)
elim non_vide_V; intros u H; clear H; try exact H.
(* Goal: forall a : AV, @ex AV (fun b : AV => R (plus a b) zero) *)
intros a; try assumption.
(* Goal: isocele O M B *)
elim angle_cons with (a := a) (u := u); intros v H0; try exact H0.
(* Goal: @ex AV (fun b : AV => R (plus a b) zero) *)
exists (cons v u).
(* Goal: R (plus a (cons v u)) zero *)
apply transitive with (plus (cons u v) (cons v u)).
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
auto.
Qed.
Parameter pisurdeux : AV.
 
Axiom double_pisurdeux : R (double pisurdeux) pi.
Hint Resolve double_pisurdeux.
 
Lemma construction_orthogonal : forall u : V, exists v : V, orthogonal v u.
(* Goal: forall u : V, @ex V (fun v : V => orthogonal v u) *)
intros u; try assumption.
(* Goal: @ex V (fun v : V => orthogonal v u) *)
cut (exists v : V, R (double (cons u v)) pi).
(* Goal: forall _ : @ex V (fun v : V => R (double (cons u v)) pi), @ex V (fun v : V => orthogonal v u) *)
(* Goal: @ex V (fun v : V => R (double (cons u v)) pi) *)
intros H; try assumption.
(* Goal: isocele O M B *)
elim H; intros v H0; clear H; try exact H0.
(* Goal: @ex V (fun v : V => and (R (cons (vec A B) u) (cons v (vec B A))) (R (cons u v) (double a))) *)
exists v.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
auto.
(* Goal: isocele O M B *)
elim angle_cons with (a := pisurdeux) (u := u); intros v H0; try exact H0.
(* Goal: @ex V (fun v : V => and (R (cons (vec A B) u) (cons v (vec B A))) (R (cons u v) (double a))) *)
exists v.
(* Goal: R (double (cons u v)) pi *)
apply transitive with (double pisurdeux).
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
auto.
Qed.
 
Lemma unicite_circonscrit :
 forall M A B O O' : PO,
 isocele O A B ->
 isocele O M B ->
 isocele O M A ->
 isocele O' A B ->
 isocele O' M B ->
 isocele O' M A ->
 (colineaire (vec O A) (vec O' A) /\ colineaire (vec O B) (vec O' B)) /\
 colineaire (vec O M) (vec O' M).
(* Goal: and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)) *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
unfold colineaire in |- *.
(* Goal: forall (M A B O O' : PO) (_ : isocele O A B) (_ : isocele O M B) (_ : isocele O M A) (_ : isocele O' A B) (_ : isocele O' M B) (_ : isocele O' M A), and (and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero)) (R (double (cons (vec O M) (vec O' M))) zero) *)
intros M A B O O' H H0 H1 H2 H3 H4.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
cut (R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B))); intros.
cut
 (R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))));
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
 intros.
cut
 (R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))));
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
 intros.
(* Goal: and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero) *)
(* Goal: R (double (cons (vec O M) (vec O' M))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
split; [ idtac | try assumption ].
(* Goal: and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero) *)
(* Goal: R (double (cons (vec O M) (vec O' M))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
split; [ idtac | try assumption ].
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (opp (vec O A)) (opp (vec O' A)))); auto.
apply
 transitive
  with
    (double
       (plus (cons (opp (vec O A)) (vec A B))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
          (cons (vec A B) (opp (vec O' A))))); auto.
apply
 transitive
  with
    (double
       (plus (cons (opp (vec O A)) (vec A B))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
          (cons (vec A B) (opp (vec O' A))))); auto.
apply
 transitive
  with
    (plus (double (cons (opp (vec O A)) (vec A B)))
       (double (cons (vec A B) (opp (vec O' A))))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (double (cons (opp (vec O A)) (vec A B)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec A B) (vec A O)))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec A B) (vec A O'))); auto.
(* Goal: R (double (cons (opp (vec O B)) (opp (vec O' B)))) (double (cons (vec B O) (vec B O'))) *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply R_double.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
apply
 transitive
  with
    (double
       (plus (cons (opp (vec O A)) (vec A B)) (cons (vec A B) (vec A O))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with (double (plus (cons (vec A O) (vec A B)) (cons (vec A B) (vec A O))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (double (cons (opp (vec O B)) (opp (vec O' B)))) (double (cons (vec B O) (vec B O'))) *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply R_double.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec B O) (vec B O'))); auto.
(* Goal: R (double (cons (opp (vec O B)) (opp (vec O' B)))) (double (cons (vec B O) (vec B O'))) *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply R_double.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (opp (vec B O)) (opp (vec B O'))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (opp (vec B O)) (opp (vec B O'))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply symetrique; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply symetrique; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply v_sym; apply opp_vect.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply v_sym; apply opp_vect.
apply
 transitive
  with (double (plus (cons (vec B O) (vec B A)) (cons (vec B A) (vec B O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (double (cons (vec B O) (vec B A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec B A) (vec B O')))); auto.
apply
 transitive
  with
    (plus (double (cons (vec B O) (vec B A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec B A) (vec B O)))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with (double (plus (cons (vec B O) (vec B A)) (cons (vec B A) (vec B O))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec M O) (vec M O'))); auto.
(* Goal: R (double (cons (opp (vec O B)) (opp (vec O' B)))) (double (cons (vec B O) (vec B O'))) *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply R_double.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (opp (vec M O)) (opp (vec M O'))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply symetrique; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
apply
 transitive
  with (double (plus (cons (vec M O) (vec M A)) (cons (vec M A) (vec M O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (double (cons (vec M O) (vec M A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec M A) (vec M O')))); auto.
apply
 transitive
  with (double (plus (cons (vec M O) (vec M A)) (cons (vec M A) (vec M O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (double (cons (vec M O) (vec M A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec M A) (vec M O')))); auto.
apply
 transitive
  with
    (plus (double (cons (vec A M) (vec A O)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec A O') (vec A M)))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with (double (plus (cons (vec A M) (vec A O)) (cons (vec A O') (vec A M))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec A O') (vec A O))); auto.
(* Goal: R (double (cons (opp (vec O B)) (opp (vec O' B)))) (double (cons (vec B O) (vec B O'))) *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply R_double.
apply
 transitive
  with (plus (cons (vec A O') (vec A M)) (cons (vec A M) (vec A O))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
cut (R (double (cons (vec A O) (vec A O'))) zero); intros.
apply regulier with (a := double (cons (vec A O) (vec A O'))) (c := zero);
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (double (plus (cons (vec A O) (vec A O')) (cons (vec A O') (vec A O))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
apply
 transitive
  with (double (plus (cons (vec A O) (vec A B)) (cons (vec A B) (vec A O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (double (cons (vec A O) (vec A B)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec A B) (vec A O')))); auto.
apply
 transitive
  with
    (plus (double (cons (vec A O) (vec A B)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec A B) (vec A O)))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with (double (plus (cons (vec A O) (vec A B)) (cons (vec A B) (vec A O))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec A B) (vec A O))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec A B) (vec A O'))); auto.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
generalize (triangle_isocele (A:=O) (B:=A) (C:=B)); intros.
apply
 regulier
  with (a := cons (vec O A) (vec O B)) (c := cons (vec O' A) (vec O' B));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with pi; auto.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
generalize (triangle_isocele (A:=O') (B:=A) (C:=B)); intros.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply symetrique; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec M A) (vec M B))); auto.
(* Goal: R (cons (vec O A) (vec O B)) (double (cons (vec M A) (vec M B))) *)
(* Goal: R (double (cons (vec M A) (vec M B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply symetrique; apply angle_inscrit; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
auto.
(* Goal: R (double (cons (vec M' A) (vec M' B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply angle_inscrit; auto.
Qed.
 
Lemma construction_isocele_base :
 forall (A B : PO) (a : AV),
 exists u : V,
   (exists v : V,
      R (cons (vec A B) u) (cons v (vec B A)) /\ R (cons u v) (double a)).
(* Goal: forall (A B : PO) (a : AV), @ex V (fun u : V => @ex V (fun v : V => and (R (cons (vec A B) u) (cons v (vec B A))) (R (cons u v) (double a)))) *)
intros A B a; try assumption.
(* Goal: not (colineaire (vec M A) (vec M B)) *)
elim exists_opp_angle with (a := a); intros a' H; try exact H.
elim angle_cons with (a := plus pisurdeux a') (u := vec A B); intros u H2;
(* Goal: circonscrit M A B O *)
(* Goal: and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
 try exact H2.
elim angle_cons with (a := cons u (vec A B)) (u := vec B A); intros v H3;
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
 try exact H3.
(* Goal: @ex V (fun u : V => @ex V (fun v : V => and (R (cons (vec A B) u) (cons v (vec B A))) (R (cons u v) (double a)))) *)
exists u.
(* Goal: @ex V (fun v : V => and (R (cons (vec A B) u) (cons v (vec B A))) (R (cons u v) (double a))) *)
exists v.
(* Goal: and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero) *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
split; [ try assumption | idtac ].
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
auto.
apply
 transitive
  with
    (plus (cons u (vec A B))
       (plus (cons (vec A B) (vec B A)) (cons (vec B A) v))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply transitive with (plus (cons u (vec A B)) (plus pi (cons (vec B A) v)));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (vec A B) (opp (vec A B))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply v_sym; apply opp_vect.
apply transitive with (plus (cons u (vec A B)) (plus (cons (vec B A) v) pi));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply transitive with (plus (cons u (vec A B)) (plus (cons u (vec A B)) pi));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 regulier
  with
    (a := plus (plus pisurdeux a') (plus pisurdeux a'))
    (c := plus (plus pisurdeux a') (plus pisurdeux a')); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (plus (cons (vec A B) u) (cons (vec A B) u))
       (plus (cons u (vec A B)) (plus (cons u (vec A B)) pi))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (plus (plus (cons (vec A B) u) (cons (vec A B) u))
       (plus (plus (cons u (vec A B)) (cons u (vec A B))) pi)); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (plus
       (plus (plus (cons (vec A B) u) (cons (vec A B) u))
          (plus (cons u (vec A B)) (cons u (vec A B)))) pi); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus
       (plus (plus (cons (vec A B) u) (cons u (vec A B)))
          (plus (cons (vec A B) u) (cons u (vec A B)))) pi); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (plus b c) (plus d d)) (plus (plus b d) (plus c d)) *)
(* Goal: R (plus (plus b d) (plus c d)) (plus (plus d b) (plus d c)) *)
apply calcul4.
apply
 transitive
  with (plus (plus (cons (vec A B) (vec A B)) (cons (vec A B) (vec A B))) pi);
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus zero zero) pi); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus (plus a a') (plus a a')) pi); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus (plus a a) (plus a' a')) pi); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (plus b c) (plus d d)) (plus (plus b d) (plus c d)) *)
(* Goal: R (plus (plus b d) (plus c d)) (plus (plus d b) (plus d c)) *)
apply calcul4.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus (double a) (plus a' a')) pi); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (double a) (plus (plus a' a') pi)); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus (plus a' a') pi) (double a)); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus a' a') (plus pisurdeux pisurdeux)); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus pisurdeux pisurdeux) (plus a' a')); auto.
(* Goal: R (plus (plus b c) (plus d d)) (plus (plus b d) (plus c d)) *)
(* Goal: R (plus (plus b d) (plus c d)) (plus (plus d b) (plus d c)) *)
apply calcul4.
Qed.
 
Lemma abba : forall A B : PO, R (cons (vec A B) (vec B A)) pi.
(* Goal: forall A B : PO, R (cons (vec A B) (vec B A)) pi *)
intros A B; try assumption.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (vec A B) (opp (vec A B))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply v_sym; apply opp_vect.
Qed.
Hint Resolve abba.
 
Lemma calcul5 :
 forall a b c d : AV,
 R (plus (plus a (plus b c)) (plus d d))
   (plus a (plus (plus d b) (plus d c))).
(* Goal: forall a b c d : AV, R (plus (plus a (plus b c)) (plus d d)) (plus a (plus (plus d b) (plus d c))) *)
intros a b c d; try assumption.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus a (plus (plus b c) (plus d d))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (plus b d) (plus c d)); auto.
(* Goal: R (plus (plus b c) (plus d d)) (plus (plus b d) (plus c d)) *)
(* Goal: R (plus (plus b d) (plus c d)) (plus (plus d b) (plus d c)) *)
apply calcul4.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
Qed.
 
Lemma construction_circonscrit_vecteur :
 forall M A B : PO,
 ex
   (fun u : V =>
    ex
      (fun v : V =>
       ex
         (fun w : V =>
          (R (cons u v) (double (cons (vec M A) (vec M B))) /\
           R (cons u w) (double (cons (vec B A) (vec B M))) /\
           R (cons v w) (double (cons (vec A B) (vec A M)))) /\
          R (cons (vec A B) u) (cons v (vec B A)) /\
          R (cons w (vec M B)) (cons (vec B M) v) /\
          R (cons (vec M A) w) (cons u (vec A M))))).
(* Goal: forall M A B : PO, @ex V (fun u : V => @ex V (fun v : V => @ex V (fun w : V => and (and (R (cons u v) (double (cons (vec M A) (vec M B)))) (and (R (cons u w) (double (cons (vec B A) (vec B M)))) (R (cons v w) (double (cons (vec A B) (vec A M)))))) (and (R (cons (vec A B) u) (cons v (vec B A))) (and (R (cons w (vec M B)) (cons (vec B M) v)) (R (cons (vec M A) w) (cons u (vec A M)))))))) *)
intros M A B; try assumption.
elim
 construction_isocele_base
  with (A := A) (B := B) (a := cons (vec M A) (vec M B)); 
(* Goal: isocele O M B *)
 intros u H; elim H; intros v H0; clear H; try exact H0.
(* Goal: R (cons (vec O A) (vec O B)) pi *)
elim H0; intros H H1; clear H0; try exact H1.
(* Goal: @ex V (fun v : V => and (R (cons (vec A B) u) (cons v (vec B A))) (R (cons u v) (double a))) *)
exists u; exists v.
elim angle_cons with (a := cons u (vec A M)) (u := vec M A); intros w H';
 try exact H'.
(* Goal: @ex V (fun w : V => and (and (R (cons u v) (double (cons (vec M A) (vec M B)))) (and (R (cons u w) (double (cons (vec B A) (vec B M)))) (R (cons v w) (double (cons (vec A B) (vec A M)))))) (and (R (cons (vec A B) u) (cons v (vec B A))) (and (R (cons w (vec M B)) (cons (vec B M) v)) (R (cons (vec M A) w) (cons u (vec A M)))))) *)
exists w.
(* Goal: and (and (R (cons u v) (double (cons (vec M A) (vec M B)))) (and (R (cons u w) (double (cons (vec B A) (vec B M)))) (R (cons v w) (double (cons (vec A B) (vec A M)))))) (and (R (cons (vec A B) u) (cons v (vec B A))) (and (R (cons w (vec M B)) (cons (vec B M) v)) (R (cons (vec M A) w) (cons u (vec A M))))) *)
generalize (somme_triangle M A B).
(* Goal: forall _ : R (plus (cons (vec M A) (vec M B)) (plus (cons (vec A B) (vec A M)) (cons (vec B M) (vec B A)))) pi, and (and (R (cons u v) (double (cons (vec M A) (vec M B)))) (and (R (cons u w) (double (cons (vec B A) (vec B M)))) (R (cons v w) (double (cons (vec A B) (vec A M)))))) (and (R (cons (vec A B) u) (cons v (vec B A))) (and (R (cons w (vec M B)) (cons (vec B M) v)) (R (cons (vec M A) w) (cons u (vec A M))))) *)
generalize (somme_pi (vec A B) u v).
(* Goal: forall (_ : R (plus (cons (vec A B) u) (plus (cons v (opp (vec A B))) (cons (opp u) (opp v)))) pi) (_ : R (plus (cons (vec M A) (vec M B)) (plus (cons (vec A B) (vec A M)) (cons (vec B M) (vec B A)))) pi), and (and (R (cons u v) (double (cons (vec M A) (vec M B)))) (and (R (cons u w) (double (cons (vec B A) (vec B M)))) (R (cons v w) (double (cons (vec A B) (vec A M)))))) (and (R (cons (vec A B) u) (cons v (vec B A))) (and (R (cons w (vec M B)) (cons (vec B M) v)) (R (cons (vec M A) w) (cons u (vec A M))))) *)
intros H2 H3; try assumption.
(* Goal: and (and (R (cons u v) (double (cons (vec M A) (vec M B)))) (and (R (cons u w) (double (cons (vec B A) (vec B M)))) (R (cons v w) (double (cons (vec A B) (vec A M)))))) (and (R (cons (vec A B) u) (cons v (vec B A))) (and (R (cons w (vec M B)) (cons (vec B M) v)) (R (cons (vec M A) w) (cons u (vec A M))))) *)
split; [ split; try assumption | try assumption ].
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
cut (R (cons u w) (double (cons (vec B A) (vec B M)))); intros.
(* Goal: and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero) *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
split; [ try assumption | idtac ].
apply regulier with (a := cons u v) (c := double (cons (vec M A) (vec M B)));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons u w); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec B A) (vec B M))); auto.
apply
 regulier
  with
    (a := double (cons (vec B M) (vec B A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
    (c := double (cons (vec B M) (vec B A))); auto.
apply
 transitive
  with
    (plus
       (plus (double (cons (vec M A) (vec M B)))
          (double (cons (vec A B) (vec A M))))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec B M) (vec B A)))); auto.
apply
 transitive
  with
    (plus (double (cons (vec M A) (vec M B)))
       (plus (double (cons (vec A B) (vec A M)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
          (double (cons (vec B M) (vec B A))))); auto.
apply
 transitive
  with
    (plus (double (cons (vec M A) (vec M B)))
       (double (plus (cons (vec A B) (vec A M)) (cons (vec B M) (vec B A)))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (double
       (plus (cons (vec M A) (vec M B))
          (plus (cons (vec A B) (vec A M)) (cons (vec B M) (vec B A)))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with (double (plus (cons (vec B M) (vec B A)) (cons (vec B A) (vec B M))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double pi); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec B M) (vec B M))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with zero; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (plus (cons u (vec A M))
       (plus (cons (vec A M) (vec M A)) (cons (vec M A) w))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply transitive with (plus (cons u (vec A M)) (plus pi (cons (vec M A) w)));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply transitive with (plus (cons u (vec A M)) (plus (cons (vec M A) w) pi));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply transitive with (plus (plus (cons u (vec A M)) (cons (vec M A) w)) pi);
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply transitive with (plus (plus (cons u (vec A M)) (cons u (vec A M))) pi);
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 regulier
  with
    (a := plus (cons (vec A B) u) (cons (vec A B) u))
    (c := plus (cons (vec A B) u) (cons (vec A B) u)); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus
       (plus (plus (cons (vec A B) u) (cons (vec A B) u))
          (plus (cons u (vec A M)) (cons u (vec A M)))) pi); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus
       (plus (plus (cons (vec A B) u) (cons u (vec A M)))
          (plus (cons (vec A B) u) (cons u (vec A M)))) pi); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply calcul4; auto.
apply
 transitive
  with (plus (plus (cons (vec A B) (vec A M)) (cons (vec A B) (vec A M))) pi);
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply regulier with (a := cons u v) (c := cons u v); auto.
apply
 transitive
  with
    (plus (plus (cons u v) (plus (cons (vec A B) u) (cons (vec A B) u)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec B A) (vec B M)))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus pi (double (cons (vec B A) (vec B M)))); auto.
apply
 transitive
  with
    (plus
       (plus (cons u v)
          (plus (cons (vec A B) (vec A M)) (cons (vec A B) (vec A M)))) pi);
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (double (cons (vec B A) (vec B M))) pi); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (plus (double (cons (vec M A) (vec M B)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec A B) (vec A M)))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 regulier
  with
    (a := double (cons (vec B M) (vec B A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
    (c := double (cons (vec B M) (vec B A))); auto.
apply
 transitive
  with
    (plus
       (plus (double (cons (vec M A) (vec M B)))
          (double (cons (vec A B) (vec A M))))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec B M) (vec B A)))); auto.
apply
 transitive
  with
    (plus (double (cons (vec M A) (vec M B)))
       (plus (double (cons (vec A B) (vec A M)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
          (double (cons (vec B M) (vec B A))))); auto.
apply
 transitive
  with
    (plus (double (cons (vec M A) (vec M B)))
       (double (plus (cons (vec A B) (vec A M)) (cons (vec B M) (vec B A)))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (double
       (plus (cons (vec M A) (vec M B))
          (plus (cons (vec A B) (vec A M)) (cons (vec B M) (vec B A)))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with (double (plus (cons (vec B M) (vec B A)) (cons (vec B A) (vec B M))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double pi); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec B M) (vec B M))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with zero; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (plus (cons (vec A B) u)
       (plus (cons v (opp (vec A B))) (cons (opp u) (opp v)))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with (plus (plus (cons (vec A B) u) (cons (vec A B) u)) (cons u v)); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (plus (cons (vec A B) u) (cons v (opp (vec A B))))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (cons (opp u) (opp v))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons v (vec B A)); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply opp_vect; auto.
(* Goal: and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero) *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
split; [ try assumption | idtac ].
(* Goal: and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero) *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
split; [ try assumption | idtac ].
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply regulier with (a := cons (vec M A) w) (c := cons u (vec A M)); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (vec M A) (vec M B)); auto.
apply
 transitive
  with
    (plus (cons u (vec A M))
       (plus (cons (vec B M) (vec B A)) (cons (vec B A) v))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (cons u (vec A M))
       (plus (cons (vec B M) (vec B A)) (cons u (vec A B)))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (cons u (vec A M))
       (plus (cons u (vec A B)) (cons (vec B M) (vec B A)))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (plus (cons u (vec A B)) (cons (vec A B) (vec A M)))
       (plus (cons u (vec A B)) (cons (vec B M) (vec B A)))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 regulier
  with (a := cons (vec M A) (vec M B)) (c := cons (vec M A) (vec M B)); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus
       (plus (cons (vec M A) (vec M B))
          (plus (cons (vec A B) (vec A M)) (cons (vec B M) (vec B A))))
       (plus (cons u (vec A B)) (cons u (vec A B)))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply transitive with (plus pi (plus (cons u (vec A B)) (cons u (vec A B))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons u v); auto.
apply
 regulier
  with
    (a := plus (cons (vec A B) u) (cons (vec A B) u))
    (c := plus (cons (vec A B) u) (cons (vec A B) u)); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with pi; auto.
apply
 transitive
  with (plus (plus (cons (vec A B) u) (cons v (vec B A))) (cons u v)); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with (plus (cons (vec A B) u) (plus (cons v (vec B A)) (cons u v))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (cons (vec A B) u)
       (plus (cons v (opp (vec A B))) (cons (opp u) (opp v)))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply v_sym; apply opp_vect.
apply
 transitive
  with
    (plus (plus pi (plus (cons u (vec A B)) (cons u (vec A B))))
       (plus (cons (vec A B) u) (cons (vec A B) u))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus pi
       (plus (plus (cons u (vec A B)) (cons u (vec A B)))
          (plus (cons (vec A B) u) (cons (vec A B) u)))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus zero pi); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus pi zero); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (plus (plus (cons u (vec A B)) (cons (vec A B) u))
       (plus (cons u (vec A B)) (cons (vec A B) u))); 
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (plus (cons u u) (cons u u)); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply calcul4; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply calcul5; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply symetrique; auto.
Qed.
 
Axiom
  construction_circonscrit :
    forall M A B : PO,
    ~ colineaire (vec M A) (vec M B) ->
    exists O : PO, isocele O A B /\ isocele O A M /\ isocele O B M.
 
Definition circonscrit (M A B O : PO) :=
  isocele O A B /\ isocele O A M /\ isocele O B M.
 
Definition sont_cocycliques (M A B M' : PO) :=
  ex
    (fun O : PO =>
     ex
       (fun O' : PO =>
        (circonscrit M A B O /\ circonscrit M' A B O') /\
        colineaire (vec O A) (vec O' A) /\ colineaire (vec O B) (vec O' B))).
 
Lemma isocele_sym : forall A B C : PO, isocele A B C -> isocele A C B.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
unfold isocele in |- *; intros.
apply
 transitive with (plus (cons (vec C B) (vec A B)) (cons (vec A B) (vec C A)));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive with (plus (cons (vec C A) (vec C B)) (cons (vec A B) (vec C A)));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (vec B C) (vec B A)); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (opp (vec C B)) (opp (vec A B))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
apply
 transitive with (plus (cons (vec A B) (vec C A)) (cons (vec C A) (vec C B)));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (vec A B) (vec C B)); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (cons (opp (vec B A)) (opp (vec B C))); auto.
(* Goal: R (cons (vec A B) (vec C B)) (cons (opp (vec B A)) (opp (vec B C))) *)
apply symetrique.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
Qed.
Hint Resolve isocele_sym.
 
Theorem reciproque_cocyclique :
 forall M A B M' : PO,
 ~ colineaire (vec M A) (vec M B) ->
 R (double (cons (vec M' A) (vec M' B))) (double (cons (vec M A) (vec M B))) ->
 sont_cocycliques M A B M'.
(* Goal: forall (M A B M' : PO) (_ : not (colineaire (vec M A) (vec M B))) (_ : R (double (cons (vec M' A) (vec M' B))) (double (cons (vec M A) (vec M B)))), sont_cocycliques M A B M' *)
unfold sont_cocycliques in |- *.
(* Goal: forall (M A B M' : PO) (_ : not (colineaire (vec M A) (vec M B))) (_ : R (double (cons (vec M' A) (vec M' B))) (double (cons (vec M A) (vec M B)))), @ex PO (fun O : PO => @ex PO (fun O' : PO => and (and (circonscrit M A B O) (circonscrit M' A B O')) (and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B))))) *)
intros M A B M' H H0; try assumption.
elim construction_circonscrit with (M := M) (A := A) (B := B);
 [ intros O H2; try exact H2 | idtac ].
(* Goal: @ex PO (fun O : PO => @ex PO (fun O' : PO => and (and (circonscrit M A B O) (circonscrit M' A B O')) (and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B))))) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
exists O.
elim construction_circonscrit with (M := M') (A := A) (B := B);
 [ intros O' H1; try exact H1 | idtac ].
(* Goal: @ex PO (fun O' : PO => and (and (circonscrit M A B O) (circonscrit M' A B O')) (and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)))) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
exists O'.
(* Goal: and (and (circonscrit M A B O) (circonscrit M' A B O')) (and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B))) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
split; [ split; [ idtac | try assumption ] | idtac ].
(* Goal: circonscrit M A B O *)
(* Goal: and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
try exact H2.
(* Goal: and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
elim H1; intros H3 H4; elim H4; intros H5 H6; clear H4 H1; try exact H5.
(* Goal: and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
elim H2; intros H1 H4; elim H4; intros H7 H8; clear H4 H2; try exact H7.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
cut (R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B))); intros.
cut
 (R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))));
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
 intros.
cut
 (R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))));
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
 intros.
(* Goal: and (colineaire (vec O A) (vec O' A)) (colineaire (vec O B) (vec O' B)) *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
unfold colineaire in |- *.
(* Goal: and (R (double (cons (vec O A) (vec O' A))) zero) (R (double (cons (vec O B) (vec O' B))) zero) *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
split; [ try assumption | idtac ].
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec A O) (vec A O'))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (opp (vec O A)) (opp (vec O' A)))); auto.
(* Goal: R (double (cons (opp (vec O B)) (opp (vec O' B)))) (double (cons (vec B O) (vec B O'))) *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply R_double.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
apply
 transitive
  with (double (plus (cons (vec A O) (vec A B)) (cons (vec A B) (vec A O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (double (cons (vec A O) (vec A B)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec A B) (vec A O')))); auto.
apply
 transitive
  with
    (plus (double (cons (vec A O) (vec A B)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec A B) (vec A O)))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with (double (plus (cons (vec A O) (vec A B)) (cons (vec A B) (vec A O))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec B O) (vec B O'))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (opp (vec O B)) (opp (vec O' B)))); auto.
(* Goal: R (double (cons (opp (vec O B)) (opp (vec O' B)))) (double (cons (vec B O) (vec B O'))) *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply R_double.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply vR_R_compatible; auto.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
(* Goal: vR (opp (vec O' B)) (vec B O') *)
(* Goal: R (double (cons (vec B O) (vec B O'))) zero *)
(* Goal: R (double (cons (vec B O) (vec B A))) (double (cons (vec B O') (vec B A))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply opp_vect.
apply
 transitive
  with (double (plus (cons (vec B O) (vec B A)) (cons (vec B A) (vec B O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with
    (plus (double (cons (vec B O) (vec B A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec B A) (vec B O')))); auto.
apply
 transitive
  with
    (plus (double (cons (vec B O') (vec B A)))
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
       (double (cons (vec B A) (vec B O')))); auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
apply
 transitive
  with
    (double (plus (cons (vec B O') (vec B A)) (cons (vec B A) (vec B O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double zero); auto.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
generalize (triangle_isocele (A:=O) (B:=A) (C:=B)); intros.
apply
 regulier
  with (a := cons (vec O A) (vec O B)) (c := cons (vec O' A) (vec O' B));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
apply
 transitive
  with (plus (cons (vec O A) (vec O B)) (double (cons (vec A B) (vec A O))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with pi; auto.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
generalize (triangle_isocele (A:=O') (B:=A) (C:=B)); intros.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply symetrique; auto.
apply
 transitive
  with
    (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O'))));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (plus (cons (vec O' A) (vec O' B)) (double (cons (vec B O') (vec B A)))) (plus (cons (vec O' A) (vec O' B)) (double (cons (vec A B) (vec A O')))) *)
(* Goal: R (double (cons (vec A B) (vec A O))) (double (cons (vec A B) (vec A O'))) *)
(* Goal: R (cons (vec O A) (vec O B)) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply compatible; auto.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
generalize (triangle_isocele (A:=O) (B:=A) (C:=B)); intros.
apply
 regulier
  with (a := cons (vec O A) (vec O B)) (c := cons (vec O' A) (vec O' B));
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
 auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with pi; auto.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
generalize (triangle_isocele (A:=O') (B:=A) (C:=B)); intros.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply symetrique; auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec M A) (vec M B))); auto.
(* Goal: R (cons (vec O A) (vec O B)) (double (cons (vec M A) (vec M B))) *)
(* Goal: R (double (cons (vec M A) (vec M B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply symetrique; apply angle_inscrit; auto.
(* Goal: R (double (cons (vec M A) (vec M B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
try exact H6.
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
generalize (triangle_isocele (A:=O') (B:=A) (C:=B)); intros.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec M' A) (vec M' B))); auto.
(* Goal: R (double (cons (vec M' A) (vec M' B))) (cons (vec O' A) (vec O' B)) *)
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply angle_inscrit; auto.
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
unfold colineaire in H.
(* Goal: not (colineaire (vec M' A) (vec M' B)) *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
unfold colineaire, not in |- *.
(* Goal: forall _ : R (double (cons (vec C A) (vec C B))) zero, False *)
(* Goal: R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B))) *)
intros H1; try assumption.
(* Goal: False *)
(* Goal: not (colineaire (vec M A) (vec M B)) *)
apply H.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec M' A) (vec M' B))); auto.
(* Goal: not (colineaire (vec M A) (vec M B)) *)
try exact H.
Qed.
 
Axiom
  cocyclicite_six :
    forall A B C D : PO,
    sont_cocycliques C A B D ->
    ex
      (fun O : PO =>
       (circonscrit C A B O /\ circonscrit D A B O) /\ isocele O C D).
 
Lemma changement_base_cocyclique :
 forall A B C D : PO,
 ~ colineaire (vec C A) (vec C B) ->
 R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B))) ->
 R (double (cons (vec A C) (vec A D))) (double (cons (vec B C) (vec B D))).
(* Goal: forall (A B C D : PO) (_ : not (colineaire (vec C A) (vec C B))) (_ : R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B)))), R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))) *)
intros A B C D H H0; try assumption.
cut
 (ex
    (fun O : PO =>
     (circonscrit C A B O /\ circonscrit D A B O) /\ isocele O C D)); 
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
 intros.
(* Goal: R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))) *)
(* Goal: @ex PO (fun O : PO => and (and (circonscrit C A B O) (circonscrit D A B O)) (isocele O C D)) *)
unfold circonscrit in H1.
elim H1; intros O H2; elim H2; intros H3 H4; elim H3; intros H5 H6; elim H6;
 intros H7 H8; elim H8; intros H9 H10; clear H8 H6 H3 H2 H1; 
 try exact H10.
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
elim H5; intros H1 H2; elim H2; intros H3 H6; clear H2 H5; try exact H3.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply (cocyclique (M:=B) (A:=C) (B:=D) (O:=O) (M':=A)); auto.
(* Goal: @ex PO (fun O : PO => and (and (circonscrit C A B O) (circonscrit D A B O)) (isocele O C D)) *)
apply cocyclicite_six.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply reciproque_cocyclique; auto.
Qed.
 
Lemma changement_base_cocyclique_2 :
 forall A B C D : PO,
 ~ colineaire (vec C A) (vec C B) ->
 R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B))) ->
 R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))).
(* Goal: forall (A B C D : PO) (_ : not (colineaire (vec C A) (vec C B))) (_ : R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B)))), R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))) *)
intros A B C D H H0; try assumption.
cut
 (ex
    (fun O : PO =>
     (circonscrit C A B O /\ circonscrit D A B O) /\ isocele O C D)); 
(* Goal: forall _ : R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi), R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
 intros.
(* Goal: R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))) *)
(* Goal: @ex PO (fun O : PO => and (and (circonscrit C A B O) (circonscrit D A B O)) (isocele O C D)) *)
unfold circonscrit in H1.
elim H1; intros O H2; elim H2; intros H3 H4; elim H3; intros H5 H6; elim H5;
 intros H7 H8; elim H8; intros H9 H10; clear H8 H5 H3 H2 H1; 
 try exact H9.
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: R (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B))) *)
(* Goal: R (plus (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus (cons (vec M A) (vec M B)) (cons (vec M A) (vec M B)))) (cons (vec O A) (vec O B)) *)
(* Goal: R (plus (cons (vec O A) (vec O B)) (plus (cons (vec M B) (vec M A)) (cons (vec M B) (vec M A)))) (plus pi pi) *)
(* Goal: isocele O M A *)
(* Goal: isocele O M B *)
elim H6; intros H1 H2; elim H2; intros H3 H5; clear H2 H6; try exact H3.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply (cocyclique (M:=D) (A:=C) (B:=A) (O:=O) (M':=B)); auto.
(* Goal: @ex PO (fun O : PO => and (and (circonscrit C A B O) (circonscrit D A B O)) (isocele O C D)) *)
apply cocyclicite_six.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply reciproque_cocyclique; auto.
Qed.
 
Axiom non_zero_pi : ~ R pi zero.
 
Lemma deux_rectangles :
 forall A B C D : PO,
 orthogonal (vec C A) (vec C B) ->
 orthogonal (vec D A) (vec D B) ->
 R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))).
(* Goal: forall (A B C D : PO) (_ : not (colineaire (vec C A) (vec C B))) (_ : R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B)))), R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))) *)
unfold orthogonal in |- *; intros A B C D H H0; try assumption.
(* Goal: R (double (cons (vec B C) (vec B A))) (double (cons (vec D C) (vec D A))) *)
apply changement_base_cocyclique_2.
(* Goal: not (colineaire (vec C A) (vec C B)) *)
(* Goal: R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B))) *)
unfold not, colineaire in |- *.
(* Goal: forall _ : R (double (cons (vec C A) (vec C B))) zero, False *)
(* Goal: R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B))) *)
intros H1; try assumption.
(* Goal: False *)
(* Goal: R (double (cons (vec C A) (vec C B))) (double (cons (vec D A) (vec D B))) *)
apply non_zero_pi.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with (double (cons (vec C A) (vec C B))); auto.
(* Goal: R (cons (vec A B) u) (cons v (vec B A)) *)
(* Goal: R (cons u v) (double a) *)
apply transitive with pi; auto.
Qed.