proposition: Lemma cltb_sound : forall x y : C, x [<] y = true -> [x] < [y].
proof: Proof. intros x y H. unfold cltb in H. apply andb_prop in H. destruct H as [H1 H2]. apply cleb_sound in H1. apply cneqb_sound in H2. apply <- (Rlt_le_neq sor). now split. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl