n m : (n | m) -> (m | n) -> n = m. Proof. intros H1 H2. destruct m; only 1: exact (H2.2^ @ nat_mul_zero_r _). destruct n; only 1: exact ((nat_mul_zero_r _)^ @ H1.2). snrapply leq_antisym; nrapply leq_divides; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes