```
{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Equality.Reasoning.Core where

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General

infix   _∎
infixr  _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
infix   begin_

_≡⟨_⟩_ : {A : Set} {y z : A} → (x : A) → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = trans p q

_≡˘⟨_⟩_ : {A : Set} {y z : A} → (x : A) → y ≡ x → y ≡ z → x ≡ z
x ≡˘⟨ p ⟩ q = trans (sym p) q

_≡⟨⟩_ : {A : Set} {y : A} → (x : A) → x ≡ y → x ≡ y
x ≡⟨⟩ q = q

_∎ : {A : Set} → (x : A) → x ≡ x
x ∎ = refl

begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
begin p = p
```