assume [A,B,C] : (point(A) & point(B) & point(C) & B!=C & A!=B & A!=C)
construct [D] : (point(D) & D!=A & D!=B & cong(A,B,B,D) & cong(B,D,D,A))
construct [M] : (line(M) & on(D,M) & on(A,M))
construct [N] : (line(N) & on(D,N) & on(B,N))
construct [K1] : (circle(K1) & center(B,K1) & onc(C,K1))
construct [G] : (point(G) & on(G,N) & onc(G,K1) & bet(D,B,G))
infer (segment_add(D,B,B,G,D,G))
infer (segment_add(D,A,B,G,D,G))
infer (cong_less(D,A,D,G))
construct [K2] : (circle(K2) & center(D,K2) & onc(G,K2))
infer (inside(A,K2))
construct [F] : (point(F) & onc(F,K2) & on(F,M) & bet(D,A,F))
infer (segment_add(D,A,A,F,D,F))
infer (cong(D,F,D,G))
infer (segment_add(D,A,B,G,D,F))
infer (cong(A,F,B,G))
infer (cong(B,G,B,C))
infer (cong(A,F,B,C))
