proposition: Lemma eqA_preserves_ang: forall a b, Q_CongA a -> EqA a b -> Q_CongA b.
proof: Proof. intros. unfold Q_CongA in *. decompose [ex and] H. exists x. exists x0. exists x1. split. assumption. split. assumption. intros. rewrite H4. unfold EqA in H0. apply H0. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid