proposition: Proposition symmetric_rel_total_order (R : nat -> nat -> Type) {p : Symmetric R} {p' : Reflexive R} : (forall n m : nat, n < m -> R n m) -> (forall n m : nat, R n m).
proof: Proof. intros A n m. destruct (@leq_dichot m n) as [m_leq_n | m_gt_n]. - apply symmetry. destruct m_leq_n. + apply reflexivity. + apply A. apply leq_S_n'. assumption. - apply A, m_gt_n. Defined.
imports: Basics Spaces.Nat.Core