(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. intros A n m. destruct (@leq_dichotomy m n) as [m_leq_n | m_gt_n]. - apply symmetry. destruct m_leq_n. + apply reflexivity. + apply A. apply leq_succ. assumption. - apply A, m_gt_n. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.