proposition: Lemma coinciders_symm : forall a b c : E, coinciders a b c = coinciders a c b.
proof: Proof. assert (forall a b c x : E, coincide_at a b c x -> coincide_at a c b x). ir. uh H; uhg; xd. assert (forall a b c : E, sub (coinciders a b c) (coinciders a c b)). ir. uf sub; ir. uf coinciders. ufi coinciders H0. Ztac. ap Z_inc. uh H2; xd. ap H. am. ir. ap extensionality. ap H0. ap H0. Qed.
imports: universe