proposition: Lemma bet_flat_ang : forall a A B C, Q_CongA a -> a A B C -> Bet A B C -> Ang_Flat a.
proof: Proof. intros. unfold Ang_Flat. split. auto. intros. assert(HH:=bet_conga__bet A B C A0 B0 C0 H1). apply HH. apply (ang_conga a); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid