proposition: Theorem eq_trans : transitive _ qeq.
proof: Proof. intros a b c Hab Hbc. destruct a as [a| ]; simpl in Hab; simpl. destruct b as [b| ]; simpl in Hab, Hbc; [ idtac | contradiction ]. destruct c as [c| ]; [ rewrite Hab; assumption | assumption ]. destruct b as [b| ]; simpl in Hab, Hbc; [ contradiction | assumption ]. Qed.
imports: Utf8 QArith Misc