proposition: Lemma leA_dec_to_eqA_dec : (forall (a b : A), leA a b \/ ~ leA a b) -> forall (a b : A), eqA a b \/ ~ eqA a b.
proof: Proof. intros leA_dec a b; elim (leA_dec a b); intro case_a_le_b. elim (leA_dec b a); intro case_b_le_a; [left | right]. split; trivial. intro H; elim H; clear H; intros H1 H2. apply case_b_le_a; trivial. right; intro H; apply case_a_le_b. elim H; trivial. Qed.
imports: CoLoR(LogicUtil) Coq(Relations)