n m d : Type0 := exists a b, a * n = d + b * m. Existing Class . Global Instance nat_bezout_refl_l n k : n k n. Proof. by exists 1, 0. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes