in progress work on ang_lt_supplementary

src/congruence/ang_lt.lean

@@ -197,4 +197,13 @@ begin
 end
 
 lemma ang_lt_supplementary {α α' β β' : ang} (hαα' : α <ₐ α')
-(hαβ : supplementary α β) (hα'β' : supplementary α' β') : β' <ₐ β := sorry
+(hαβ : supplementary α β) (hα'β' : supplementary α' β') : β' <ₐ β :=
+begin
+  rw supplementary at hαβ, 
+  obtain ⟨⟨a,b,c,d,α,β,hcad⟩,hα,hβ⟩ := hαβ,
+  rw supplementary at hα'β',
+  obtain ⟨⟨a,b',d,c,α',β',hcad'⟩,hα',hβ'⟩ := hα'β',
+  rw ang_lt at hαα',
+  obtain ⟨b',c,a,_,_,_⟩ := hαα',
+  sorry,
+end

src/order/angle.lean

@@ -42,6 +42,12 @@ structure ray := (vertex : pts) (inside : set pts)
 /--A ray can be defined by explicitly stating the vertex `o` and `a`. -/
 def two_pt_ray (o a : pts) : ray := ⟨o, {x : pts | same_side_pt o a x} ∪ {o}, ⟨a, rfl⟩⟩
 
+/--A flipped ray is defined using between. -/
+def flip_ray (r : ray) : ray :=
+begin
+  sorry,
+end
+
 notation a`-ᵣ`b := two_pt_ray a b
 
 lemma two_pt_ray_vertex (o a : pts) : (o-ᵣa).vertex = o := rfl