class EuclidGeom.CevaCfgClass (P : outParam (Type u_1)) [outParam (EuclidGeom.EuclideanPlane P)] : Type u_1

• A : P
• B : P
• C : P
• D : P
• abd_nd : ¬EuclidGeom.Collinear EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.D
• bcd_nd : ¬EuclidGeom.Collinear EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.D
• cad_nd : ¬EuclidGeom.Collinear EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.D
• a_ne_b : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B
• b_ne_c : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C
• c_ne_a : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A
• d_ne_a : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.A
• d_ne_b : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.B
• d_ne_c : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.C
• ba_npara_cd : ¬EuclidGeom.Parallel (LIN EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.A) (LIN EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.D)
• cb_npara_ad : ¬EuclidGeom.Parallel (LIN EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.B) (LIN EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.D)
• ac_npara_bd : ¬EuclidGeom.Parallel (LIN EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.C) (LIN EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.D)
• E : P
• e_def : EuclidGeom.CevaCfgClass.E = EuclidGeom.Line.inx (LIN EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.B) (LIN EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.D) (_ : ¬EuclidGeom.Parallel (LIN EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.B) (LIN EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.D))
• F : P
• f_def : EuclidGeom.CevaCfgClass.F = EuclidGeom.Line.inx (LIN EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.C) (LIN EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.D) (_ : ¬EuclidGeom.Parallel (LIN EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.C) (LIN EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.D))
• G : P
• g_def : EuclidGeom.CevaCfgClass.G = EuclidGeom.Line.inx (LIN EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.A) (LIN EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.D) (_ : ¬EuclidGeom.Parallel (LIN EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.A) (LIN EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.D))

theorem EuclidGeom.CevaCfgClass.ncolin_dca {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : ¬EuclidGeom.Collinear EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A

theorem EuclidGeom.CevaCfgClass.colin_ebc {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.Collinear EuclidGeom.CevaCfgClass.E EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C

theorem EuclidGeom.CevaCfgClass.colin_eda {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.Collinear EuclidGeom.CevaCfgClass.E EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.A

instance EuclidGeom.CevaCfgClass.c_ne_e {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.E

Equations

• (_ : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.E) = (_ : Fact (EuclidGeom.CevaCfgClass.C ≠ EuclidGeom.CevaCfgClass.E))

theorem EuclidGeom.CevaCfgClass.dratio_ebc_eq_wedge_div_wedge {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.divratio EuclidGeom.CevaCfgClass.E EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C = EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.A / EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A

theorem EuclidGeom.CevaCfgClass.ncolin_dab {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : ¬EuclidGeom.Collinear EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B

theorem EuclidGeom.CevaCfgClass.colin_fca {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.Collinear EuclidGeom.CevaCfgClass.F EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A

theorem EuclidGeom.CevaCfgClass.colin_fdb {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.Collinear EuclidGeom.CevaCfgClass.F EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.B

instance EuclidGeom.CevaCfgClass.a_ne_f {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.F

Equations

• (_ : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.F) = (_ : Fact (EuclidGeom.CevaCfgClass.A ≠ EuclidGeom.CevaCfgClass.F))

theorem EuclidGeom.CevaCfgClass.dratio_fca_eq_wedge_div_wedge {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.divratio EuclidGeom.CevaCfgClass.F EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A = EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.B / EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B

theorem EuclidGeom.CevaCfgClass.ncolin_dbc {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : ¬EuclidGeom.Collinear EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C

theorem EuclidGeom.CevaCfgClass.colin_gab {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.Collinear EuclidGeom.CevaCfgClass.G EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B

theorem EuclidGeom.CevaCfgClass.colin_gdc {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.Collinear EuclidGeom.CevaCfgClass.G EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.C

instance EuclidGeom.CevaCfgClass.b_ne_g {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.G

Equations

• (_ : EuclidGeom.PtNe EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.G) = (_ : Fact (EuclidGeom.CevaCfgClass.B ≠ EuclidGeom.CevaCfgClass.G))

theorem EuclidGeom.CevaCfgClass.dratio_gab_eq_wedge_div_wedge {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.divratio EuclidGeom.CevaCfgClass.G EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B = EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.C / EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C

theorem EuclidGeom.CevaCfgClass.wedge_div_wedge_mul_eq_minus_one {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.A / EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A * (EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.B / EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B) * (EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.C / EuclidGeom.wedge EuclidGeom.CevaCfgClass.D EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C) = -1

theorem EuclidGeom.CevaCfgClass.ceva_theorem {P : Type u_1} [EuclidGeom.EuclideanPlane P] [cfg : EuclidGeom.CevaCfgClass P] : EuclidGeom.divratio EuclidGeom.CevaCfgClass.E EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C * EuclidGeom.divratio EuclidGeom.CevaCfgClass.F EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A * EuclidGeom.divratio EuclidGeom.CevaCfgClass.G EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B = -1

def EuclidGeom.CevaCfg (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

Equations

• EuclidGeom.CevaCfg P = EuclidGeom.CevaCfgClass P

theorem EuclidGeom.CevaCfg.ceva_theorem {P : Type u_1} [EuclidGeom.EuclideanPlane P] (cfg : EuclidGeom.CevaCfg P) : EuclidGeom.divratio EuclidGeom.CevaCfgClass.E EuclidGeom.CevaCfgClass.B EuclidGeom.CevaCfgClass.C * EuclidGeom.divratio EuclidGeom.CevaCfgClass.F EuclidGeom.CevaCfgClass.C EuclidGeom.CevaCfgClass.A * EuclidGeom.divratio EuclidGeom.CevaCfgClass.G EuclidGeom.CevaCfgClass.A EuclidGeom.CevaCfgClass.B = -1

theorem EuclidGeom.ceva_theorem {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (abd_nd : ¬EuclidGeom.Collinear A B D) (bcd_nd : ¬EuclidGeom.Collinear B C D) (cad_nd : ¬EuclidGeom.Collinear C A D) (ba_npara_cd : ¬EuclidGeom.Parallel (LIN B A (_ : A ≠ B)) (LIN C D (_ : D ≠ C))) (cb_npara_ad : ¬EuclidGeom.Parallel (LIN C B (_ : B ≠ C)) (LIN A D (_ : D ≠ A))) (ac_npara_bd : ¬EuclidGeom.Parallel (LIN A C (_ : C ≠ A)) (LIN B D (_ : D ≠ B))) (E : P) (e_def : E = EuclidGeom.Line.inx (LIN C B (_ : B ≠ C)) (LIN A D (_ : D ≠ A)) cb_npara_ad) (F : P) (f_def : F = EuclidGeom.Line.inx (LIN A C (_ : C ≠ A)) (LIN B D (_ : D ≠ B)) ac_npara_bd) (G : P) (g_def : G = EuclidGeom.Line.inx (LIN B A (_ : A ≠ B)) (LIN C D (_ : D ≠ C)) ba_npara_cd) : EuclidGeom.divratio E B C * EuclidGeom.divratio F C A * EuclidGeom.divratio G A B = -1