# Library HighSchoolGeometry.coplanarite

Require Export alignement.
Set Implicit Arguments.
Unset Strict Implicit.

Definition coplanaires1 (A B C D : PO) :=
a : R,
( b : R,
cons 1 D =
add_PP (cons a A) (add_PP (cons b B) (cons (1 + - (a + b)) C))).

Lemma vecteur_def_coplanaires1 :
(k k' : R) (A B C D : PO),
vec A D = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C))
coplanaires1 A B C D.
unfold coplanaires1, vec in |- *; intros.
(1 + - (k + k')); auto.
k; auto.
RingPP2 H.
RingPP.
Qed.

Lemma coplanaires1_vecteur_def :
A B C D : PO,
coplanaires1 A B C D
k : R,
( k' : R,
vec A D = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C))).
unfold coplanaires1, vec in |- *; intros.
elim H; intros a H0; elim H0; intros b H1; try clear H0 H; try exact H1.
b; auto.
(1 + - (a + b)); auto.
rewrite H1.
RingPP.
Qed.

Definition coplanaires (A B C D : PO) :=
alignes A B C coplanaires1 A B C D.

Lemma coplanaires_trivial : A B C : PO, coplanaires A B C A.
unfold coplanaires, coplanaires1 in |- *; intros.
right; try assumption.
1; 0.
RingPP.
Qed.

Lemma coplanaires_trivial2 : A B C : PO, coplanaires A B C B.
unfold coplanaires, coplanaires1 in |- *; intros.
right; try assumption.
0; 1.
RingPP.
Qed.

Lemma coplanaires_trivial3 : A B C : PO, coplanaires A B C C.
unfold coplanaires, coplanaires1 in |- *; intros.
right; try assumption.
0; 0.
RingPP.
Qed.
Hint Resolve coplanaires_trivial coplanaires_trivial2 coplanaires_trivial3:
geo.

Ltac hcoplanaires H x y :=
elim H; clear H; intros H;
[ tauto || idtac
| elim (coplanaires1_vecteur_def H); clear H; intros x H; elim H; clear H;
intros y H ].

Ltac hPPcoplanaires H x y :=
elim H; clear H; intros H;
[ tauto || idtac
| elim H; clear H; intros x H; elim H; clear H; intros y H ].

Lemma non_coplanaires_expl :
A B C D : PO,
¬ coplanaires A B C D ¬ alignes A B C ¬ coplanaires1 A B C D.
unfold coplanaires in |- *; intros.
intuition.
Qed.

Axiom
repere_espace :
A B C D E : PO,
¬ coplanaires A B C D
a : R,
( b : R,
( c : R,
cons 1 E =
(add_PP (cons c C) (cons (1 + - (a + b + c)) D)))).
Hint Unfold coplanaires: geo.

Lemma vecteur_def_coplanaires :
(k k' : R) (A B C D : PO),
vec A D = add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C))
coplanaires A B C D.
intros; unfold coplanaires in |- ×.
right; try assumption.
apply vecteur_def_coplanaires1 with (k := k) (k' := k'); try assumption.
Qed.

Lemma alignes_coplanaires :
A B C D : PO, alignes A B C coplanaires A B D C.
intros.
halignes H ipattern:a.
apply vecteur_def_coplanaires with (k := a) (k' := 0).
rewrite H0.
Ringvec.
Qed.
Hint Resolve alignes_coplanaires: geo.

Lemma coplanaire_ordre_permute :
A B C D : PO, coplanaires A B C D coplanaires A B D C.
intros.
elim H; clear H; intros; auto with geo.
elim (coplanaires1_vecteur_def H); intros.
elim H0; [ intros y H1; try clear H0; try exact H1 ].
elim (classic (y = 0)); intros.
assert (alignes A B D); auto with geo.
apply colineaire_alignes with x.
rewrite H1; rewrite H0; Ringvec.
apply vecteur_def_coplanaires with (k := / y × - x) (k' := / y).
rewrite H1.
Fieldvec y.
Qed.

Lemma coplanaire_ordre_cycle :
A B C D : PO, coplanaires A B C D coplanaires B C D A.
intros.
elim H; clear H; intros; auto with geo.
elim coplanaires1_vecteur_def with (A := A) (B := B) (C := C) (D := D);
[ intros x H0; elim H0;
[ intros y H1; try clear H0 coplanaires1_vecteur_def; try exact H1 ]
| auto ].
elim (classic (y = 1 + - x)); intros.
rewrite H2 in H1.
assert (alignes B C D); auto with geo.
apply colineaire_alignes with (1 + - x).
VReplace (vec B D) (add_PP (vec B A) (vec A D)).
rewrite H1.
Ringvec.
assert (1 + - x + - y 0).
contrapose H0.
RReplace y (y + 0).
rewrite <- H3; ring.
apply
vecteur_def_coplanaires
with (k := / (1 + - x + - y) × - y) (k' := / (1 + - x + - y)).
VReplace (vec B D) (add_PP (vec B A) (vec A D)).
rewrite H1.
Fieldvec (1 + - x + - y).
Qed.
Hint Resolve coplanaire_ordre_cycle coplanaire_ordre_permute: geo.

Lemma coplanaire_trans :
A B C D E : PO,
¬ alignes A B C
coplanaires A B C D coplanaires A B C E coplanaires B C D E.
intros.
elim H1; clear H1; intros.
tauto.
elim H0; clear H0; intros.
tauto.
elim coplanaires1_vecteur_def with (A := A) (B := B) (C := C) (D := D);
[ intros x H2; elim H2; [ intros y H3; try clear H2; try exact H3 ] | auto ].
elim coplanaires1_vecteur_def with (A := A) (B := B) (C := C) (D := E);
[ intros k H4; elim H4; [ intros k' H5; try clear H4; try exact H5 ]
| auto ].
elim (classic (y = 1 + - x)); intros.
rewrite H2 in H3.
assert (alignes B C D); auto with geo.
apply colineaire_alignes with (1 + - x).
VReplace (vec B D) (add_PP (vec B A) (vec A D)).
rewrite H3.
Ringvec.
assert (1 + - x + - y 0).
contrapose H0.
RReplace y (y + 0).
rewrite <- H4; ring.
assert
(vec B A =
add_PP (mult_PP (/ (1 + - x + - y) × - y) (vec B C))
(mult_PP (/ (1 + - x + - y)) (vec B D))).
VReplace (vec B D) (add_PP (vec B A) (vec A D)).
rewrite H3.
Fieldvec (1 + - x + - y).
assert
(vec B E =
add_PP (mult_PP (1 + - k + - k') (vec B A)) (mult_PP k' (vec B C))).
VReplace (vec B E) (add_PP (vec B A) (vec A E)).
rewrite H5.
Ringvec.
apply
vecteur_def_coplanaires
with
(k := k' + / (1 + - x + - y) × - y × (1 + - k + - k'))
(k' := / (1 + - x + - y) × (1 + - k + - k')).
rewrite H7; rewrite H6.
Fieldvec (1 + - x + - y).
Qed.