proposition: Lemma le_lt_equiv_dec {A:Type} {le : relation A} {P0: TotalPreOrder le} {dec : RelDecision le} (a b:A) : le a b -> {lt a b}+{preorder_equiv a b}.
proof: Proof. intro H; destruct (decide (le b a)). - right;split;auto. - left;split;auto. Defined.