proposition: Lemma extension_gradexp : forall {Tm: Tarski_neutral_dimensionless} {TmEQD : Tarski_neutral_dimensionless_with_decidable_point_equality Tm} P Q (f : @Tpoint Tn -> @Tpoint Tm), line_extension f P Q -> forall A B X, Col P Q A -> Col P Q B -> GradExp (f A) X (f B) -> exists C, Col P Q C /\ GradExp A C B /\ f C = X.
proof: Proof. intros Tm TmEQD P Q f [HPQ [fInj [fBet fCong]]] A B X HA HB. remember (f A) as fA; remember (f B) as fB; rewrite gradexp__gradexpinv. intro HI; induction HI as [|fA fB C C' ? ? ? HInd]; [exists B; repeat split; [auto|constructor|auto]|]. rename C into X, C' into X'; destruct HInd as [C [? []]]; auto. destruct (midpoint_existence A C) as [C' []]; exists C'. assert (Col P Q C') by (destruct (eq_dec_points A C); [treat_equalities|apply (colx A C)]; Col). split; [auto|split; [|apply l7_17 with fA fB; split; subst; auto]]. rewrite gradexp__gradexpinv; apply gradexpinv_stab with C; auto. rewrite <- gradexp__gradexpinv; assumption. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.completeness GeoCoq.Meta_theory.Continuity.grad GeoCoq.Tarski_dev.Ch08_orthogonality