proposition: Lemma bleRat_total : forall r1 r2, bleRat r1 r2 = false -> bleRat r2 r1 = true.
proof: Proof. intuition. unfold bleRat in *. rattac. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms