proposition: Lemma lexprod_irreflex : forall a, a >lex a -> False.
proof: Proof. intros a gt_aa; inversion gt_aa. absurd (gtL a0 a0); auto with sets. absurd (gtR b b); auto with sets. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)