proposition: Lemma extension_grad : 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 -> Grad (f A) (f B) X -> exists C, Col P Q C /\ Grad A B C /\ f C = X.
proof: Proof. intros Tm TmEQD P Q f [HPQ [fInj [fBet fCong]]] A B X HA HB HGrad. elim (eq_dec_points A B); [intro; subst; apply grad112__eq in HGrad; subst|]; [exists B; repeat split; [auto|constructor]|intro HAB]. remember (f A) as fA; remember (f B) as fB. induction HGrad as [|fA fB C C' ? HInd ? ?]; [exists B; repeat split; [auto|constructor|auto]|]. rename C into X, C' into X'; destruct HInd as [C [? []]]; trivial. destruct (segment_construction A C A B) as [C' []]; exists C'. assert (Col P Q C') by (apply (colx A C); Col; apply grad_neq__neq13 with B; auto). split; [auto|split; [apply grad_stab with C; Cong|]]. apply (construction_uniqueness fA X fA fB); Cong; [|subst; auto..]. intro; subst X; assert (A = C) by (apply fInj; auto; congruence). subst; apply grad121__eq, fInj in HGrad; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.completeness GeoCoq.Meta_theory.Continuity.grad GeoCoq.Tarski_dev.Ch08_orthogonality